Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 14:37 68dbf27c

View on Github →

feat(number_theory): the class group of an integral closure is finite (#9059) This is essentially the proof that the ring of integers of a global field has a finite class group, apart from filling in each hypothesis.

Estimated changes

Created src/number_theory/class_number/finite.lean

added theorem class_group.exists_mem_finset_approx'

added theorem class_group.exists_mem_finset_approx

added theorem class_group.exists_min

added theorem class_group.exists_mk0_eq_mk0

added theorem class_group.finset_approx.zero_not_mem

added theorem class_group.mem_finset_approx

added theorem class_group.mk_M_mem_surjective

added theorem class_group.ne_bot_of_prod_finset_approx_mem

added theorem class_group.norm_bound_pos

added theorem class_group.norm_le

added theorem class_group.norm_lt

added theorem class_group.prod_finset_approx_ne_zero

Modified src/ring_theory/algebraic.lean

added theorem is_integral_closure.exists_smul_eq_mul