Documentation Verification Report

IntegralDomain

📁 Source: Mathlib/RingTheory/IntegralDomain.lean

Statistics

Metric	Count
Definitions `divisionRingOfIsDomain`, `fieldOfDomain`, `groupWithZeroOfCancel`	3
Theorems `isField_of_domain`, `exists_eq_pow_of_mul_eq_pow_of_coprime`, `div_eq_quo_add_rem_div`, `card_nthRoots_subgroup_units`, `exists_eq_pow_of_mul_eq_pow_of_coprime`, `instIsCyclicUnitsOfFinite`, `isCyclic_of_injective_ringHom`, `isCyclic_of_subgroup_isDomain`, `isCyclic_subgroup_units`, `mul_left_bijective_of_finite₀`, `mul_right_bijective_of_finite₀`, `subgroup_units_cyclic`, `sum_hom_units`, `sum_hom_units_eq_zero`	14
Total	17

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isField_of_domain` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`nonempty_fintype` `Field.toIsField`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_pow_of_mul_eq_pow_of_coprime` 📖	mathematical	`IsCoprime` `prod` `CommSemiring.toCommMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Finset` `SetLike.instMembership` `instSetLike`	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`exists_eq_pow_of_mul_eq_pow_of_coprime` `IsCoprime.prod_right` `erase_subset` `notMem_erase` `prod_insert` `insert_erase`

Fintype

Definitions

Name	Category	Theorems
`divisionRingOfIsDomain` 📖	CompOp	—
`fieldOfDomain` 📖	CompOp	—
`groupWithZeroOfCancel` 📖	CompOp	—

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_eq_quo_add_rem_div` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`degree_modByMonic_lt` `IsDomain.toNontrivial` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `Monic.ne_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `add_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `modByMonic_add_div`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_nthRoots_subgroup_units` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike`	`Finset.card` `Finset.filter` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finset.univ` `Multiset.card` `Polynomial.nthRoots` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike`	—	`Finset.card_le_card_of_injOn` `map_pow` `MonoidHom.instMonoidHomClass` `Finset.coe_filter` `Function.Injective.injOn` `Multiset.toFinset_card_le`
`exists_eq_pow_of_mul_eq_pow_of_coprime` 📖	mathematical	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`exists_eq_pow_of_mul_eq_pow` `isUnit_of_dvd_one` `dvd_add` `Distrib.leftDistribClass` `dvd_mul_of_dvd_right` `GCDMonoid.gcd_dvd_left` `GCDMonoid.gcd_dvd_right`
`instIsCyclicUnitsOfFinite` 📖	mathematical	—	`IsCyclic` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`isCyclic_of_injective_ringHom` `Units.val_injective`
`isCyclic_of_injective_ringHom` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`nonempty_fintype` `isCyclic_of_card_pow_eq_one_le` `le_trans` `card_nthRoots_subgroup_units` `Polynomial.card_nthRoots`
`isCyclic_of_subgroup_isDomain` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_of_injective_ringHom`
`isCyclic_subgroup_units` 📖	mathematical	—	`IsCyclic` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpow`	—	`isCyclic_of_injective_ringHom` `Units.val_injective` `Subtype.val_injective`
`mul_left_bijective_of_finite₀` 📖	mathematical	—	`Function.Bijective` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Finite.injective_iff_bijective` `mul_left_injective₀`
`mul_right_bijective_of_finite₀` 📖	mathematical	—	`Function.Bijective` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Finite.injective_iff_bijective` `mul_right_injective₀`
`subgroup_units_cyclic` 📖	mathematical	—	`IsCyclic` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpow`	—	`isCyclic_subgroup_units`
`sum_hom_units` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instOneMonoidHom` `Fintype.card`	—	`Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul` `mul_one` `Nat.cast_zero` `sum_hom_units_eq_zero`
`sum_hom_units_eq_zero` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsCyclic.exists_monoid_generator` `Finite.of_fintype` `isCyclic_subgroup_units` `sub_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `MonoidHom.ext` `one_pow` `Finset.sum_comp` `Finset.sum_congr` `MonoidHom.card_fiber_eq_of_mem_range` `MonoidHom.instMonoidHomClass` `MonoidHom.map_one` `Finset.sum_subtype` `Finset.smul_sum` `Finset.sum_nbij` `Finset.coe_range` `pow_injOn_Iio_orderOf` `Finset.mem_range` `orderOf_pos` `pow_mod_orderOf` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `MulZeroClass.zero_mul` `geom_sum_mul` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Nat.cast_one` `Nat.cast_zero` `pow_orderOf_eq_one` `sub_self` `smul_zero`

---

← Back to Index