leanprover-community/mathlib3

Pull Requests Commits

feat(number_theory): the class number is finite if there is an admissible absolute value

Vierkantor committed 4 years ago

25b1b1ba

feat(linear_algebra/matrix): absolute values and matrices

Vierkantor committed 4 years ago

e243ec0f

Vierkantor committed 4 years ago

be907f6c

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

Vierkantor committed 4 years ago

359173d3

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

Vierkantor committed 4 years ago

93d14967

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

Vierkantor committed 4 years ago

79b49420

Vierkantor committed 4 years ago

173e6b29

Make `euclidean_absolute_value` a predicate on absolute values

Vierkantor committed 4 years ago

4291be5d

Vierkantor committed 4 years ago

f9813186

feat(algebra): define "Euclidean" absolute values

Vierkantor committed 4 years ago

b694d4f5

Remove `number_field` assumption from `ring_of_integers`

Vierkantor committed 4 years ago

61cb23a2

Clarify comment

Vierkantor committed 4 years ago

dcb5a388

Add `integrally_closed` and `is_integral_closure` instances

Vierkantor committed 4 years ago

8ce6a838

Move `char_zero.of_algebra` to appropriate file

Vierkantor committed 4 years ago

95187a63

These are uneligible for `@[ext]` because of explicit vars

Vierkantor committed 4 years ago

33b95d12

Better `ext` lemmas

Vierkantor committed 4 years ago

4ad2b9d1

Vierkantor committed 4 years ago

0ab26bca

Why not just make it an instance directly

Vierkantor committed 4 years ago

0e3d02e8

Style fix Authors: line

Vierkantor committed 4 years ago

82227073

feat(number_theory): define number fields, function fields, and the ring of integers

Vierkantor committed 4 years ago

e8bdbcd6

feat(algebra/group/hom_instance): additive endomorphisms form a ring (#8954)

eric-wieser committed 4 years ago

1dddd7f9

refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902)

jcommelin committed 4 years ago

2fa82513

feat(category_theory/limits/kan_extension): Prove (co)reflectivity for Kan extensions (#8962)

adamtopaz committed 4 years ago

289e6dc6

chore(analysis/convex/basic): generalize `concave_on.le_on_segment` to monoids (#8959)

pechersky committed 4 years ago

8da6699f

feat(ring_theory/dedekind_domain): the integral closure of a DD is a DD (#8847)

Vierkantor committed 4 years ago

9d3e3e8a

feat(order/bounded_lattice): `ne_(bot|top)_iff_exists` (#8960)

pechersky committed 4 years ago

6c247315

feat(group_theory): Add `monoid_hom.mker` and generalise the codomain for `monoid_hom.ker` (#8532)

shingtaklam1324 committed 4 years ago

07c57b56

feat(tactic/lint): minor linter improvements (#8934)

fpvandoorn committed 4 years ago

0b8a858f

chore(algebra,group_theory,right_theory,linear_algebra): add missing lemmas (#8948)

eric-wieser committed 4 years ago

9b000466

fix(category_theory/adjunction/basic): Fix typo in docstring (#8950)

justus-springer committed 4 years ago

2beaa28a

Older