Documentation Verification Report

Conductor

📁 Source: Mathlib/RingTheory/Conductor.lean

Statistics

Metric	Count
Definitions `conductor`, `quotAdjoinEquivQuotMap`	2
Theorems `localRingHom_bijective_of_not_conductor_le`, `adjoin_eq_top_of_conductor_eq_top`, `comap_map_eq_map_adjoin_of_coprime_conductor`, `conductor_eq_of_eq`, `conductor_eq_top_iff_adjoin_eq_top`, `conductor_eq_top_of_adjoin_eq_top`, `conductor_eq_top_of_powerBasis`, `conductor_subset_adjoin`, `mem_coeSubmodule_conductor`, `mem_conductor_iff`, `prod_mem_ideal_map_of_mem_conductor`, `quotAdjoinEquivQuotMap_apply_mk`	12
Total	14

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`localRingHom_bijective_of_not_conductor_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `conductor` `Algebra.adjoin` `Set` `Set.instSingletonSet`	`Function.Bijective` `AtPrime` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommSemiring` `DFunLike.coe` `RingHom` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `localRingHom` `algebraMap` `Subalgebra.toAlgebra` `Algebra.id` `Ideal.over_def`	—	`Ideal.over_def` `SetLike.not_le_iff_exists` `instIsConcreteLE` `localRingHom_bijective_of_saturated_inf_eq_top` `top_le_iff` `mul_one`

(root)

Definitions

Name	Category	Theorems
`conductor` 📖	CompOp	12 math math: `RingOfIntegers.exponent_eq_sInf`, `isStronglyTranscendental_mk_radical_conductor`, `mem_conductor_iff`, `RingOfIntegers.not_dvd_exponent_iff`, `conductor_subset_adjoin`, `conductor_eq_of_eq`, `mem_coeSubmodule_conductor`, `conductor_mul_differentIdeal`, `conductor_eq_top_iff_adjoin_eq_top`, `conductor_eq_top_of_powerBasis`, `conductor_eq_top_of_adjoin_eq_top`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`
`quotAdjoinEquivQuotMap` 📖	CompOp	1 math math: `quotAdjoinEquivQuotMap_apply_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_eq_top_of_conductor_eq_top` 📖	mathematical	`conductor` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Algebra.eq_top_iff` `mem_conductor_iff` `Ideal.eq_top_iff_one` `one_mul`
`comap_map_eq_map_adjoin_of_coprime_conductor` 📖	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` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra`	`Ideal.map` `Subalgebra.toSemiring` `Subalgebra.algebra`	—	`RingHom.instRingHomClass` `le_antisymm` `Submodule.mem_sup` `Ideal.eq_top_iff_one` `Distrib.rightDistribClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_mul` `Set.mem_image` `Algebra.algebraMap_eq_smul_one` `Submonoid.mk_smul` `smul_eq_mul` `mul_one` `prod_mem_ideal_map_of_mem_conductor` `Ideal.mem_comap` `Ideal.add_mem` `mul_comm` `Ideal.mul_mem_left` `Ideal.mem_map_of_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsScalarTower.algebraMap_eq` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Ideal.map_map` `Ideal.le_comap_map`
`conductor_eq_of_eq` 📖	mathematical	`SetLike.coe` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet`	`conductor`	—	`Ideal.ext` `Set.ext_iff`
`conductor_eq_top_iff_adjoin_eq_top` 📖	mathematical	—	`conductor` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`adjoin_eq_top_of_conductor_eq_top` `conductor_eq_top_of_adjoin_eq_top`
`conductor_eq_top_of_adjoin_eq_top` 📖	mathematical	`Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`conductor` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Zero.instNonempty`
`conductor_eq_top_of_powerBasis` 📖	mathematical	—	`conductor` `PowerBasis.gen` `CommRing.toRing` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`conductor_eq_top_of_adjoin_eq_top` `PowerBasis.adjoin_gen_eq_top`
`conductor_subset_adjoin` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `conductor` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.instSingletonSet`	—	`mul_one`
`mem_coeSubmodule_conductor` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `IsLocalization.coeSubmodule` `conductor` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`subsingleton_or_nontrivial` `Unique.instSubsingleton` `Subalgebra.subsingleton_of_subsingleton` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `mul_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHom.map_adjoin` `Set.image_singleton`
`mem_conductor_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `conductor` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`prod_mem_ideal_map_of_mem_conductor` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `conductor` `Ideal.map`	`Set` `Set.instMembership` `Set.image` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.instSingletonSet` `DFunLike.coe` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra` `Algebra.id` `SetLike.coe` `Subalgebra.toSemiring` `Subalgebra.algebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingHom.instRingHomClass` `Finsupp.mem_span_image_iff_linearCombination` `Ideal.span.eq_1` `Ideal.map.eq_1` `Finsupp.linearCombination_apply` `mul_comm` `Finsupp.sum_mul` `smul_eq_mul` `mul_assoc` `Set.mem_image` `mem_conductor_iff` `Ideal.mem_comap` `Ideal.mul_mem_left` `Ideal.mem_map_of_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Finset.sum_induction` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Ideal.add_mem` `SetLike.mem_coe` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Ideal.zero_mem` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finsupp.mem_supported`
`quotAdjoinEquivQuotMap_apply_mk` 📖	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` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `Polynomial.instCommSemiringAdjoinSingleton` `Subalgebra.toAlgebra`	`RingEquiv` `HasQuotient.Quotient` `Subalgebra.toSemiring` `Ideal.instHasQuotient_1` `Polynomial.instCommRingAdjoinSingleton` `CommRing.toRing` `Ideal.map` `Subalgebra.algebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotAdjoinEquivQuotMap` `Ring.toSemiring` `Subalgebra.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1`

---

← Back to Index