Commit 2023-06-24 15:15 0e58ccac

View on Github →

feat: port NumberTheory.ClassNumber.Finite (#5337)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ClassNumber/Finite.lean

added theorem ClassGroup.exists_mem_finsetApprox

added theorem ClassGroup.exists_mem_finset_approx'

added theorem ClassGroup.exists_min

added theorem ClassGroup.exists_mk0_eq_mk0

added theorem ClassGroup.finsetApprox.zero_not_mem

added theorem ClassGroup.mem_finsetApprox

added theorem ClassGroup.mkMMem_surjective

added theorem ClassGroup.ne_bot_of_prod_finsetApprox_mem

added theorem ClassGroup.normBound_pos

added theorem ClassGroup.norm_le

added theorem ClassGroup.norm_lt

added theorem ClassGroup.prod_finsetApprox_ne_zero