Documentation Verification Report

KummerDedekind

📁 Source: Mathlib/NumberTheory/KummerDedekind.lean

Statistics

Metric	Count
Definitions `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk`, `quotMapEquivQuotQuotMap`	2
Theorems `irreducible_map_of_irreducible_minpoly`, `emultiplicity_factors_map_eq_emultiplicity`, `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span`, `normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map`, `quotMapEquivQuotQuotMap_symm_apply`	5
Total	7

KummerDedekind

Definitions

Name	Category	Theorems
`normalizedFactorsMapEquivNormalizedFactorsMinPolyMk` 📖	CompOp	4 math math: `emultiplicity_factors_map_eq_emultiplicity`, `normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span`
`quotMapEquivQuotQuotMap` 📖	CompOp	1 math math: `quotMapEquivQuotQuotMap_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emultiplicity_factors_map_eq_emultiplicity` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `Ideal.map`	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Polynomial` `HasQuotient.Quotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Polynomial.semiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Set` `Set.instMembership` `setOf` `Polynomial.commSemiring` `Ideal.Quotient.commSemiring` `Polynomial.instNormalizationMonoid` `Ideal.Quotient.commRing` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `NormalizedGCDMonoid.toNormalizationMonoid` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Ideal.Quotient.field` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.commRing` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Ideal.Quotient.instRingQuotient` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `Polynomial.map` `minpoly` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk`	—	`RingHom.instRingHomClass` `Ideal.uniqueFactorizationMonoid` `Ideal.instIsTwoSided_1` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.eq_1` `Equiv.coe_trans` `IsPrincipalIdealRing.isDedekindDomain` `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity` `normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity`
`normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span` 📖	mathematical	`Polynomial` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `Polynomial.commSemiring` `Ideal.Quotient.commSemiring` `Polynomial.instNormalizationMonoid` `Ideal.Quotient.commRing` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `CommRing.toCommSemiring` `NormalizedGCDMonoid.toNormalizationMonoid` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Ideal.Quotient.field` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.commRing` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Ideal.Quotient.instRingQuotient` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `Polynomial.map` `minpoly` `CommSemiring.toSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsIntegral`	`Set` `Set.instMembership` `setOf` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `DFunLike.coe` `Equiv` `Set.Elem` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk` `Ideal.span` `Set.instUnion` `SetLike.coe` `Submodule.setLike` `Set.instSingletonSet` `AlgHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `RingHom.instRingHomClass` `Ideal.uniqueFactorizationMonoid` `normalizedFactorsEquivOfQuotEquiv_symm` `Ideal.comap.congr_simp` `Ideal.map_span` `Set.image_singleton` `Set.image_congr` `quotMapEquivQuotQuotMap_symm_apply` `le_antisymm` `Ideal.mem_span_singleton` `Ideal.mem_comap` `Ideal.Quotient.mk_surjective` `Set.union_comm` `Ideal.span_union` `Ideal.span_eq` `Ideal.mem_span_singleton_sup` `Ideal.Quotient.mk_eq_mk_iff_sub_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Ideal.span_le` `Set.union_subset_iff` `Ideal.le_comap_of_map_le` `Ideal.map_quotient_self`
`normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing`	`UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `Multiset.map` `Set.Elem` `Polynomial` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `setOf` `Multiset` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Multiset.instMembership` `Polynomial.commSemiring` `Ideal.Quotient.commSemiring` `Polynomial.instNormalizationMonoid` `Ideal.Quotient.commRing` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `NormalizedGCDMonoid.toNormalizationMonoid` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Ideal.Quotient.field` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.commRing` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Ideal.Quotient.instRingQuotient` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `Polynomial.map` `minpoly` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `normalizedFactorsMapEquivNormalizedFactorsMinPolyMk` `Multiset.attach`	—	`RingHom.instRingHomClass` `Multiset.ext'` `Ideal.uniqueFactorizationMonoid` `Ideal.instIsTwoSided_1` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `emultiplicity_factors_map_eq_emultiplicity` `UniqueFactorizationMonoid.normalize_normalized_factor` `Subtype.prop` `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors` `UniqueFactorizationMonoid.irreducible_of_normalized_factor` `Polynomial.map_monic_ne_zero` `minpoly.monic` `EuclideanDomain.toNontrivial` `bot_eq_zero` `Submodule.instCanonicallyOrderedAdd` `Ideal.map_eq_bot_iff_of_injective` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Equiv.symm_apply_apply` `Multiset.count_map_eq_count'` `Subtype.coe_injective` `Equiv.injective` `Multiset.count_attach` `Multiset.count_eq_zero` `Multiset.mem_map`
`quotMapEquivQuotQuotMap_symm_apply` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing`	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Polynomial` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Polynomial.semiring` `Polynomial.commRing` `Ideal.Quotient.commRing` `Ideal.span` `Set` `Set.instSingletonSet` `Polynomial.map` `minpoly` `Ideal.map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `quotMapEquivQuotQuotMap` `Polynomial.ring` `Ideal.Quotient.instRingQuotient` `AlgHom` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval`	—	`RingHom.instRingHomClass` `RingEquiv.injective` `Ideal.instIsTwoSided_1` `IsDedekindDomain.toIsDomain` `quotMapEquivQuotQuotMap.eq_1` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.toRingEquiv_eq_coe` `RingEquiv.symm_trans_apply` `RingEquiv.symm_symm` `RingEquiv.coe_trans` `RingEquiv.symm_apply_apply` `Ideal.quotEquivOfEq_symm` `FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `RingEquiv.apply_symm_apply` `SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin.powerBasis'_gen` `Polynomial.coe_aeval_mk_apply`

KummerDedekind.Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_map_of_irreducible_minpoly` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing` `Irreducible` `Polynomial` `HasQuotient.Quotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.map` `minpoly`	`IdemSemiring.toSemiring` `Ideal.map`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `Ideal.Quotient.isDomain` `EuclideanDomain.to_principal_ideal_domain` `UniqueFactorizationMonoid.normalizedFactors_irreducible` `Ideal.uniqueFactorizationMonoid` `KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map` `Multiset.map_eq_singleton` `Multiset.map_injective` `Subtype.coe_injective` `Multiset.attach_map_val` `Multiset.map_singleton` `UniqueFactorizationMonoid.prod_normalizedFactors` `bot_eq_zero` `Submodule.instCanonicallyOrderedAdd` `Ideal.map_eq_bot_iff_of_injective` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Multiset.prod_singleton` `associated_iff_eq` `Unique.instSubsingleton` `UniqueFactorizationMonoid.irreducible_of_normalized_factor`

---

← Back to Index