Commit 2023-06-07 12:41 549bb594

View on Github →

feat: port RingTheory.ClassGroup (#4732) Some proofs are really slow and need a lot of heartbeats to complete (up to 600000).

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/ClassGroup.lean

added theorem ClassGroup.equiv_mk0

added theorem ClassGroup.equiv_mk

added theorem ClassGroup.induction

added theorem ClassGroup.mk0_eq_mk0_iff

added theorem ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring

added theorem ClassGroup.mk0_eq_one_iff

added theorem ClassGroup.mk0_surjective

added theorem ClassGroup.mk_canonicalEquiv

added theorem ClassGroup.mk_eq_mk

added theorem ClassGroup.mk_eq_mk_of_coe_ideal

added theorem ClassGroup.mk_eq_one_iff

added theorem ClassGroup.mk_eq_one_of_coe_ideal

added theorem ClassGroup.mk_mk0

added def ClassGroup

added theorem FractionalIdeal.canonicalEquiv_mk0

added theorem FractionalIdeal.coe_mk0

added theorem FractionalIdeal.map_canonicalEquiv_mk0

added theorem card_classGroup_eq_one

added theorem card_classGroup_eq_one_iff

added theorem coe_toPrincipalIdeal

added theorem mem_principal_ideals_iff

added theorem toPrincipalIdeal_eq_iff