ClassGroup

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean

Statistics

Metric	Count
Definitions ClassGroup	1
Theorems isPrincipal_of_exists_mul_ne_zero_isPrincipal, subsingleton_classGroup	2
Total	3

NormalizedGCDMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipal_of_exists_mul_ne_zero_isPrincipal 📖	—	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal Submodule.mul IsScalarTower.right Algebra.id	—	—	IsScalarTower.right Submodule.IsPrincipal.principal Submodule.mem_span_mul_finite_of_mem_mul Ideal.span_eq IsScalarTower.left Ideal.span_mul_span Ideal.instIsTwoSided_1 Ideal.span_mono Set.mul_subset_mul_right Ideal.span_le Ideal.mem_span_singleton Finset.gcd_dvd Ideal.mul_mono_right le_antisymm Ideal.mul_le mul_assoc dvd_mul_of_dvd_left Finset.gcd_mul_left Finset.dvd_gcd_iff Ideal.span.eq_1 Ideal.mul_mem_mul Dvd.dvd.trans Associated.dvd' Associated.mul_right associated_normalize Ideal.span_singleton_le_iff_mem Ideal.mem_mul_span_singleton Mathlib.Tactic.Contrapose.contrapose₄ MulZeroClass.mul_zero Ideal.span_singleton_mul_span_singleton
subsingleton_classGroup 📖	mathematical	—	ClassGroup	—	ClassGroup.induction Localization.isLocalization ClassGroup.mk_eq_one_iff

(root)

Definitions

Name	Category	Theorems
ClassGroup 📖	CompOp	32 math math: ClassGroup.mk0_integralRep, ClassGroup.mk0_eq_mk0_iff, ClassGroup.mk_eq_mk_of_coe_ideal, ClassGroup.Quot_mk_eq_mk, WeierstrassCurve.Affine.Point.toClass_zero, ClassGroup.mk0_eq_one_iff, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, ClassGroup.mkMMem_surjective, card_classGroup_eq_one_iff, ClassGroup.mk_mk0, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, ClassGroup.mk_eq_one_iff, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', ClassGroup.mk_eq_mk, ClassGroup.equivPic_symm_apply, WeierstrassCurve.Affine.Point.toClass_some, NormalizedGCDMonoid.subsingleton_classGroup, NumberField.exists_ideal_in_class_of_norm_le, WeierstrassCurve.Affine.Point.toClass_injective, ClassGroup.exists_mk0_eq_mk0, ClassGroup.mk0_surjective, ClassGroup.mk_eq_one_of_coe_ideal, WeierstrassCurve.Affine.Point.toClass_eq_zero, ClassGroup.equiv_mk0, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, ClassGroup.mk0_eq_mk0_inv_iff, ClassGroup.mk_canonicalEquiv, ClassGroup.equivPic_apply, card_classGroup_eq_one, ClassGroup.mk_def, WeierstrassCurve.Affine.Point.toClass_apply, ClassGroup.equiv_mk

---

← Back to Index