leanprover-community/mathlib3

Pull Requests Commits

feat(number_theory): define the class number of global fields

Vierkantor committed 4 years ago

fcee723c

feat(ring_theory): the surjective image of a PID is a PID

Vierkantor committed 4 years ago

6e61d08e

feat(ring_theory): `map f (span s) = span (f '' s)`

Vierkantor committed 4 years ago

9e2da6c4

chore(ring_theory): typo fix

Vierkantor committed 4 years ago

2b61bf03

feat(number_theory): the ring of integers is a Dedekind domain

Vierkantor committed 4 years ago

d4ab959a

feat(field_theory/separable): a finite field extension in char 0 is separable

Vierkantor committed 4 years ago

55648abc

feat(ring_theory): PIDs are Dedekind domains

Vierkantor committed 4 years ago

5b6bc7b0

feat(number_theory): the class group of an integral closure is finite

Vierkantor committed 4 years ago

28c57ffd

feat(ring_theory): fractions with integral denominator can be reduced

Vierkantor committed 4 years ago

ff48cd59

Vierkantor committed 4 years ago

4fa7a201

feat(number_theory/class_number): define "admissible" absolute values

Vierkantor committed 4 years ago

79bf30e0

feat(algebra/absolute_value): generalize from field to ring

Vierkantor committed 4 years ago

a003f786

feat(data/polynomial/degree): `(n : ℕ) < p.degree ↔ n < p.nat_degree`

Vierkantor committed 4 years ago

42df1860

feat(linear_algebra/matrix): some bounds on the determinant of matrices

Vierkantor committed 4 years ago

bf2301b4

feat(algebra/big_operators): absolute values and big operators

Vierkantor committed 4 years ago

adb763be

feat(data/int): absolute values and integers

Vierkantor committed 4 years ago

805a50ae

feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s

Vierkantor committed 4 years ago

8829a0a2

feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors

Vierkantor committed 4 years ago

0e8b06c0

feat(data/finset): monotone maps preserve the maximum of a finset

Vierkantor committed 4 years ago

9e8bac05

feat(ring_theory/norm): `norm R x = 0 ↔ x = 0`

Vierkantor committed 4 years ago

121b699f

feat(linear_algebra/basis): a nontrivial module has nonempty bases

Vierkantor committed 4 years ago

9dade65a

feat(linear_algebra/matrix): `M` maps some `v ≠ 0` to zero iff `det M = 0`

Vierkantor committed 4 years ago

595a3822

feat(ring_theory): non-zero divisors are not zero

Vierkantor committed 4 years ago

93600fcf

Fix, but now correctly fix

Vierkantor committed 4 years ago

9776e223

Fix variable implicitness

Vierkantor committed 4 years ago

8d2855db

feat(algebra/algebra): lemmas connecting `basis ι R A`, `no_zero_smul_divisors R A` and `injective (algebra_map R A)`

Vierkantor committed 4 years ago

bda3a79e

feat(data/polynomial/eval): leval, eval as linear map (#8999)

jcommelin committed 4 years ago

c5636921

lint(tactic/*): break long lines (#8973)

YaelDillies committed 4 years ago

1f103908

refactor(*): replace `function.swap` by `swap` (#8612)

fpvandoorn committed 4 years ago

1bc59c99

feat(group_theory/coset): Interaction between quotient_group.mk and right multiplication by elements of the subgroup (#8970)

tb65536 committed 4 years ago

a3997288

Older