Documentation Verification Report

ChainOfDivisors

📁 Source: Mathlib/RingTheory/ChainOfDivisors.lean

Statistics

Metric	Count
Definitions `mkFactorOrderIsoOfFactorDvdEquiv`	1
Theorems `isAtom_iff`, `card_subset_divisors_le_length_of_chain`, `element_of_chain_eq_pow_second_of_chain`, `element_of_chain_not_isUnit_of_index_ne_zero`, `eq_pow_second_of_chain_of_has_chain`, `eq_second_of_chain_of_prime_dvd`, `exists_chain_of_prime_pow`, `first_of_chain_isUnit`, `isPrimePow_of_has_chain`, `second_of_chain_is_irreducible`, `coe_factor_orderIso_map_eq_one_iff`, `emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors`, `emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso`, `emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso`, `factor_orderIso_map_one_eq_bot`, `map_prime_of_factor_orderIso`, `mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors`, `mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors`, `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe`, `mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe`, `pow_image_of_prime_by_factor_orderIso_dvd`	21
Total	22

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAtom_iff` 📖	mathematical	—	`IsAtom` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instPreorder` `CommMonoidWithZero.toCommMonoid` `instOrderBot` `Irreducible` `instCommMonoidWithZero`	—	`IsAtom.le_iff` `isUnit_iff_eq_one` `isUnit_of_associated_mul` `instIsCancelMulZero` `Associated.refl` `Irreducible.not_isUnit` `Irreducible.isUnit_or_isUnit` `bot_eq_one` `mul_assoc` `IsUnit.mul_val_inv` `mul_one`

DivisorChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_subset_divisors_le_length_of_chain` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid`	`Finset.card`	—	`Finset.mem_image` `Finset.mem_univ` `Finset.card_fin` `LE.le.trans` `Finset.card_le_card` `Finset.card_image_le`
`element_of_chain_eq_pow_second_of_chain` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Associates.instCommMonoidWithZero`	`Monoid.toNatPow`	—	`Unique.instSubsingleton` `Associates.ufm` `Multiset.eq_replicate_of_mem` `eq_second_of_chain_of_prime_dvd` `UniqueFactorizationMonoid.toIsCancelMulZero` `UniqueFactorizationMonoid.prime_of_normalized_factor` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `UniqueFactorizationMonoid.prod_normalizedFactors` `ne_zero_of_dvd_ne_zero` `Multiset.prod_replicate` `associated_iff_eq` `Finset.card_fin` `Finset.card_image_iff` `Set.injOn_of_injective` `pow_injective_of_not_isUnit` `Associates.instIsCancelMulZero` `element_of_chain_not_isUnit_of_index_ne_zero` `Fin.instNeZeroHAddNatOfNat_mathlib` `Irreducible.ne_zero` `second_of_chain_is_irreducible` `dvd_trans` `pow_mul_pow_sub` `card_subset_divisors_le_length_of_chain`
`element_of_chain_not_isUnit_of_index_ne_zero` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid`	`IsUnit` `Associates.instCommMonoidWithZero`	—	`DvdNotUnit.not_unit` `Associates.dvdNotUnit_iff_lt`
`eq_pow_second_of_chain_of_has_chain` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE`	`Monoid.toNatPow` `Associates.instCommMonoidWithZero`	—	`element_of_chain_eq_pow_second_of_chain` `dvd_refl` `LE.le.antisymm'` `Fin.prop` `Finset.card_fin` `Finset.card_image_iff` `Function.Injective.injOn` `StrictMono.injective` `Finset.card_le_card` `Finset.mem_image` `dvd_prime_pow` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.toIsCancelMulZero` `irreducible_iff_prime` `Associates.instDecompositionMonoid` `UniqueFactorizationMonoid.instDecompositionMonoid` `second_of_chain_is_irreducible` `Finset.mem_univ` `associated_iff_eq` `Unique.instSubsingleton` `Finset.card_image_le`
`eq_second_of_chain_of_prime_dvd` 📖	—	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE` `Prime` `Associates.instCommMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	—	`dvd_trans` `eq_of_le_of_not_lt'` `Fin.le_iff_val_le_val` `Prime.not_unit` `first_of_chain_isUnit` `not_irreducible_of_not_unit_dvdNotUnit` `DvdNotUnit.not_unit` `Associates.dvdNotUnit_iff_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Prime.irreducible` `Associates.instIsCancelMulZero`
`exists_chain_of_prime_pow` 📖	mathematical	`Prime` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associates.instCommMonoidWithZero`	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE` `Monoid.toNatPow`	—	`Fin.coe_ofNat_eq_mod` `pow_one` `Associates.dvdNotUnit_iff_lt` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Associates.instNoZeroDivisors` `Prime.ne_zero` `not_isUnit_of_not_isUnit_dvd` `Prime.not_unit` `dvd_pow` `dvd_rfl` `LT.lt.ne'` `pow_mul_pow_sub` `LT.lt.le` `dvd_prime_pow` `Associates.instIsCancelMulZero` `associated_iff_eq` `Unique.instSubsingleton`
`first_of_chain_isUnit` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE`	`IsUnit` `Associates.instCommMonoidWithZero`	—	`Associates.one_le` `Associates.isUnit_iff_eq_one` `Associates.le_one_iff` `StrictMono.monotone`
`isPrimePow_of_has_chain` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE`	`IsPrimePow` `Associates.instCommMonoidWithZero`	—	`irreducible_iff_prime` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.toIsCancelMulZero` `Associates.instDecompositionMonoid` `UniqueFactorizationMonoid.instDecompositionMonoid` `second_of_chain_is_irreducible` `zero_lt_iff` `eq_pow_second_of_chain_of_has_chain`
`second_of_chain_is_irreducible` 📖	mathematical	`StrictMono` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `Preorder.toLE`	`Irreducible` `Associates.instCommMonoidWithZero`	—	`Associates.isAtom_iff` `ne_zero_of_dvd_ne_zero` `ne_bot_of_gt` `LE.le.trans` `LT.lt.le` `Associates.isUnit_iff_eq_one` `first_of_chain_isUnit` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `StrictMono.lt_iff_lt`

(root)

Definitions

Name	Category	Theorems
`mkFactorOrderIsoOfFactorDvdEquiv` 📖	CompOp	2 math math: `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe`, `mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_factor_orderIso_map_eq_one_iff` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid`	`Set` `Set.instMembership` `Set.Iic` `DFunLike.coe` `OrderIso` `Set.Elem` `instFunLikeOrderIso` `Associates.instOne`	—	`Subtype.prop` `Subtype.coe_eta` `OrderIso.symm_apply_apply` `one_dvd` `factor_orderIso_map_one_eq_bot`
`emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors` 📖	mathematical	`Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `NormalizationMonoid.ofUniqueUnits` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`emultiplicity` `MonoidWithZero.toMonoid` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors`	—	`UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `normalize_eq` `UniqueFactorizationMonoid.toIsCancelMulZero` `associatesEquivOfUniqueUnits_symm_apply` `Associates.mk_le_mk_of_dvd` `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe` `emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso` `Associates.mk_ne_zero` `Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd` `Prime.irreducible` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.prime_of_normalized_factor` `associated_iff_eq` `emultiplicity_mk_eq_emultiplicity`
`emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `Associates.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `Associates.uniqueUnits` `CommMonoidWithZero.toCommMonoid` `Associates.ufm`	`emultiplicity` `Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `instFunLikeOrderIso` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `CommMonoid.toMonoid`	—	`Unique.instSubsingleton` `Associates.ufm` `le_antisymm` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso` `mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors` `Subtype.coe_eta` `UniqueFactorizationMonoid.toIsCancelMulZero` `OrderIso.symm_apply_apply`
`emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `Associates.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `Associates.uniqueUnits` `CommMonoidWithZero.toCommMonoid` `Associates.ufm`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `DFunLike.coe` `OrderIso` `Set.Elem` `instFunLikeOrderIso` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `CommMonoid.toMonoid`	—	`Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `emultiplicity_zero` `UniqueFactorizationMonoid.normalizedFactors.congr_simp` `UniqueFactorizationMonoid.normalizedFactors_zero` `FiniteMultiplicity.emultiplicity_eq_multiplicity` `FiniteMultiplicity.of_prime_left` `Associates.instIsCancelMulZero` `WfDvdMonoid.wfDvdMonoid_associates` `UniqueFactorizationMonoid.toIsWellFounded` `UniqueFactorizationMonoid.prime_of_normalized_factor` `pow_dvd_iff_le_emultiplicity` `pow_image_of_prime_by_factor_orderIso_dvd` `pow_multiplicity_dvd`
`factor_orderIso_map_one_eq_bot` 📖	mathematical	—	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `Associates.instOne` `one_dvd` `Associates.instCommMonoidWithZero`	—	`one_dvd` `bot_le` `Subtype.mk_bot` `BotHomClass.map_bot` `OrderIsoClass.toBotHomClass` `OrderIso.instOrderIsoClass`
`map_prime_of_factor_orderIso` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `Associates.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `Associates.uniqueUnits` `CommMonoidWithZero.toCommMonoid` `Associates.ufm`	`Prime` `Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `instFunLikeOrderIso` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `CommMonoid.toMonoid`	—	`Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `irreducible_iff_prime` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.toIsCancelMulZero` `Associates.instDecompositionMonoid` `UniqueFactorizationMonoid.instDecompositionMonoid` `Associates.isAtom_iff` `ne_zero_of_dvd_ne_zero` `Subtype.prop` `Associates.isUnit_iff_eq_bot` `Associates.isUnit_iff_eq_one` `coe_factor_orderIso_map_eq_one_iff` `Prime.not_unit` `UniqueFactorizationMonoid.prime_of_normalized_factor` `isUnit_one` `le_trans` `le_of_lt` `OrderIso.surjective` `Subtype.mk_eq_bot_iff` `Prime.ne_zero` `UniqueFactorizationMonoid.irreducible_of_normalized_factor` `OrderIso.lt_iff_lt` `OrderIso.map_bot`
`mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors` 📖	mathematical	`Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `NormalizationMonoid.ofUniqueUnits` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors`	—	`normalize_eq` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `UniqueFactorizationMonoid.toIsCancelMulZero` `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe` `map_prime_of_factor_orderIso` `Associates.mk_ne_zero` `Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd` `Prime.irreducible` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.prime_of_normalized_factor` `Associates.mk_le_mk_of_dvd` `associated_iff_eq` `Subtype.prop`
`mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `Associates.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `Associates.uniqueUnits` `CommMonoidWithZero.toCommMonoid` `Associates.ufm`	`Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `instFunLikeOrderIso` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `CommMonoid.toMonoid`	—	`Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd` `Prime.irreducible` `Associates.instIsCancelMulZero` `UniqueFactorizationMonoid.toIsCancelMulZero` `map_prime_of_factor_orderIso` `Subtype.prop` `associated_iff_eq`
`mkFactorOrderIsoOfFactorDvdEquiv_apply_coe` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Associates` `MonoidWithZero.toMonoid` `Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `RelIso` `Set.Elem` `Preorder.toLE` `RelIso.instFunLike` `mkFactorOrderIsoOfFactorDvdEquiv` `MulEquiv` `Associates.instMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulEquiv.instEquivLike` `associatesEquivOfUniqueUnits`	—	—
`mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Associates` `MonoidWithZero.toMonoid` `Set` `Set.instMembership` `Set.Iic` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid` `RelIso` `Set.Elem` `Preorder.toLE` `RelIso.instFunLike` `RelIso.symm` `mkFactorOrderIsoOfFactorDvdEquiv` `Equiv.symm` `MulEquiv` `Associates.instMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulEquiv.instEquivLike` `associatesEquivOfUniqueUnits`	—	—
`pow_image_of_prime_by_factor_orderIso_dvd` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `Associates.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `Associates.uniqueUnits` `CommMonoidWithZero.toCommMonoid` `Associates.ufm` `Preorder.toLE` `Associates.instPreorder` `Monoid.toNatPow`	`Set` `Set.instMembership` `Set.Iic` `DFunLike.coe` `OrderIso` `Set.Elem` `instFunLikeOrderIso` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `CommMonoid.toMonoid`	—	`Unique.instSubsingleton` `Associates.ufm` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `pow_zero` `DivisorChain.exists_chain_of_prime_pow` `UniqueFactorizationMonoid.prime_of_normalized_factor` `le_trans` `DivisorChain.eq_pow_second_of_chain_of_has_chain` `Subtype.coe_lt_coe` `OrderIso.lt_iff_lt` `StrictMono.lt_iff_lt` `LE.le.trans` `OrderIso.symm_apply_apply` `OrderIso.le_iff_le` `Subtype.coe_eta` `OrderIso.apply_symm_apply` `Subtype.coe_le_coe` `ne_zero_of_dvd_ne_zero` `Subtype.prop`

---

← Back to Index