RelNorm

📁 Source: Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Statistics

Metric	Count
Definitions `relNorm`, `spanNorm`	2
Theorems `absNorm_algebraMap`, `absNorm_relNorm`, `exists_relNorm_eq_pow_of_isPrime`, `intNorm_mem_spanNorm`, `le_spanNorm_spanNorm`, `map_relNorm`, `map_spanIntNorm`, `norm_mem_relNorm`, `norm_mem_spanNorm`, `relNorm_algebraMap`, `relNorm_algebraMap'`, `relNorm_apply`, `relNorm_bot`, `relNorm_comap_algEquiv`, `relNorm_eq_bot_iff`, `relNorm_eq_pow_of_isMaximal`, `relNorm_eq_pow_of_isPrime_isGalois`, `relNorm_int`, `relNorm_le_comap`, `relNorm_map_algEquiv`, `relNorm_mono`, `relNorm_relNorm`, `relNorm_singleton`, `relNorm_smul`, `relNorm_top`, `spanIntNorm_localization`, `spanNorm_bot`, `spanNorm_eq`, `spanNorm_eq_bot_iff`, `spanNorm_le_comap`, `spanNorm_mono`, `spanNorm_mul`, `spanNorm_mul_of_bot_or_top`, `spanNorm_mul_spanNorm_le`, `spanNorm_singleton`, `spanNorm_spanNorm`, `spanNorm_spanNorm_of_bot_or_top`, `spanNorm_top`	38
Total	40

Ideal

Definitions

Name	Category	Theorems
`relNorm` 📖	CompOp	21 math math: `relNorm_smul`, `relNorm_mono`, `relNorm_relNorm`, `relNorm_top`, `relNorm_eq_pow_of_isPrime_isGalois`, `relNorm_singleton`, `map_relNorm`, `relNorm_le_comap`, `exists_relNorm_eq_pow_of_isPrime`, `relNorm_algebraMap'`, `relNorm_int`, `spanNorm_eq`, `relNorm_algebraMap`, `relNorm_eq_bot_iff`, `relNorm_apply`, `relNorm_bot`, `norm_mem_relNorm`, `absNorm_relNorm`, `relNorm_map_algEquiv`, `relNorm_eq_pow_of_isMaximal`, `relNorm_comap_algEquiv`
`spanNorm` 📖	CompOp	17 math math: `spanNorm_spanNorm`, `intNorm_mem_spanNorm`, `map_spanIntNorm`, `spanNorm_mono`, `spanIntNorm_localization`, `spanNorm_spanNorm_of_bot_or_top`, `le_spanNorm_spanNorm`, `spanNorm_eq`, `spanNorm_mul`, `norm_mem_spanNorm`, `spanNorm_singleton`, `spanNorm_bot`, `spanNorm_le_comap`, `spanNorm_mul_spanNorm_le`, `spanNorm_eq_bot_iff`, `spanNorm_mul_of_bot_or_top`, `spanNorm_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `map` `RingHom` `RingHom.instFunLike` `algebraMap` `Monoid.toNatPow` `Nat.instMonoid` `Module.finrank` `FractionRing` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `OreLocalization.instAlgebra` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero`	—	`IsDomain.toNontrivial` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Int.instIsDomain` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Module.free_of_finite_type_torsion_free'` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `instIsTorsionFreeIntOfIsAddTorsionFree` `Int.instIsAddTorsionFree` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Module.IsReflexive.to_isTorsionFree` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `absNorm_relNorm` `PerfectField.ofCharZero` `IsFractionRing.charZero` `Int.instCharZero` `IsDedekindDomain.toIsDomain` `relNorm_relNorm` `AddCommGroup.intIsScalarTower` `IsScalarTower.right` `relNorm_algebraMap` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`absNorm_relNorm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `relNorm`	—	`Module.Finite.left` `isNoetherian_of_isNoetherianRing_of_finite` `IsDedekindDomainDvr.toIsNoetherian` `Int.instIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `AddCommGroup.intIsScalarTower` `IsDomain.toNontrivial` `relNorm_bot` `absNorm_bot` `uniqueFactorizationMonoid` `prod_normalizedFactors_eq_self` `Multiset.prod_induction` `IsScalarTower.right` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `one_eq_top` `relNorm_top` `absNorm_top` `UniqueFactorizationMonoid.ne_zero_of_mem_normalizedFactors` `Ring.DimensionLEOne.maximalOfPrime` `IsDedekindDomainDvr.ring_dimensionLEOne` `mem_normalizedFactors_iff` `Int.instNontrivial` `Module.free_of_finite_type_torsion_free'` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `instIsTorsionFreeIntOfIsAddTorsionFree` `Int.instIsAddTorsionFree` `under_ne_bot` `Algebra.IsIntegral.of_finite` `LiesOver.trans` `Int.liesOver_span_absNorm` `Nat.absNorm_under_prime` `IsPrime.under` `IsMaximal.isPrime'` `Nat.prime_iff_prime_int` `relNorm_eq_pow_of_isMaximal` `IsMaximal.under` `map_pow` `IsDedekindDomain.toIsDomain` `absNorm_eq_pow_inertiaDeg` `inertiaDeg_algebra_tower` `Int.ideal_span_isMaximal_of_prime` `pow_mul`
`exists_relNorm_eq_pow_of_isPrime` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eq_bot_of_liesOver_bot` `Algebra.IsIntegral.of_finite` `IsDomain.toNontrivial` `relNorm_bot` `IsScalarTower.left` `bot_pow` `one_ne_zero` `relNorm_mono` `map_le_iff_le_comap` `le_of_eq` `liesOver_iff` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `dvd_prime_pow` `isCancelMulZero` `prime_of_isPrime` `IsScalarTower.right` `dvd_iff_le` `relNorm_algebraMap` `associated_iff_eq` `Unique.instSubsingleton`
`intNorm_mem_spanNorm` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`spanNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing`	—	`subset_span` `Algebra.IsIntegral.of_finite` `Set.mem_image_of_mem`
`le_spanNorm_spanNorm` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `spanNorm`	—	`span_mono` `Algebra.IsIntegral.of_finite` `subset_span` `Set.mem_image_of_mem` `Algebra.intNorm_intNorm`
`map_relNorm` 📖	mathematical	—	`map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `span` `Set.image` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`map_spanIntNorm`
`map_spanIntNorm` 📖	mathematical	—	`map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `spanNorm` `span` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Algebra.IsIntegral.of_finite` `spanNorm.eq_1` `map.eq_1` `map_span` `RingHom.instRingHomClass` `Set.image_image` `Set.image_congr`
`norm_mem_relNorm` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm`	—	`norm_mem_spanNorm`
`norm_mem_spanNorm` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`spanNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm`	—	`subset_span` `Algebra.intNorm_eq_norm`
`relNorm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `map` `RingHom` `RingHom.instFunLike` `algebraMap` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Module.finrank` `FractionRing` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `OreLocalization.instCommSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `OreLocalization.instAlgebra` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial`	—	`IsScalarTower.right` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `spanNorm_eq` `eq_of_localization_maximal` `IsMaximal.isPrime'` `IsLocalization.isDomain_of_local_atPrime` `IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Localization.AtPrime.isDedekindDomain` `instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl` `instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` `Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain` `spanIntNorm_localization` `primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `OreLocalization.instIsScalarTower` `Localization.isLocalization` `map_pow` `RingHom.instRingHomClass` `map_map` `IsScalarTower.algebraMap_eq` `IsPrincipalIdealRing.principal` `IsDedekindDomain.isPrincipalIdealRing` `Localization.AtPrime.isLocalRing` `span_singleton_generator` `map_span` `Set.image_singleton` `Algebra.IsIntegral.of_finite` `spanNorm_singleton` `IsScalarTower.left` `span_singleton_pow` `instIsTwoSided_1` `IsFractionRing.injective` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `instIsFractionRingAtPrimeFractionRing` `Algebra.algebraMap_intNorm` `instIsScalarTowerAtPrimeFractionRing` `instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing` `IsIntegralClosure.of_isIntegrallyClosed` `instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing` `instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` `instFiniteDimensionalFractionRingOfFinite` `IsScalarTower.algebraMap_apply` `Algebra.norm_algebraMap` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`relNorm_algebraMap'` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `map` `RingHom` `RingHom.instFunLike` `algebraMap` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Module.finrank` `FractionRing` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toModule` `OreLocalization.instCommSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `OreLocalization.instAlgebra` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial`	—	`IsScalarTower.right` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `relNorm_algebraMap` `map_map` `IsScalarTower.algebraMap_eq`
`relNorm_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `span` `Set.image` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	—
`relNorm_bot` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`relNorm_comap_algEquiv` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `comap` `AlgEquiv` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `EquivLike.toFunLike` `AlgEquiv.instEquivLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsDedekindDomain.toIsDomain`	—	`IsDedekindDomain.toIsDomain` `relNorm_map_algEquiv` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_symm`
`relNorm_eq_bot_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`spanNorm_eq_bot_iff`
`relNorm_eq_pow_of_isMaximal` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `inertiaDeg`	—	`IsScalarTower.right` `exists_maximal_ideal_liesOver_of_isIntegral` `Algebra.IsIntegral.of_finite` `Ring.instFiniteNormalClosure` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Ring.instNontrivialNormalClosure` `Ring.instIsTorsionFreeNormalClosure` `LiesOver.trans` `Ring.instIsScalarTowerNormalClosure` `Ring.instIsDomainNormalClosure` `Ring.instIsIntegrallyClosedNormalClosure` `Ring.instFiniteNormalClosure_1` `FaithfulSMul.to_isTorsionFree` `Ring.instFaithfulSMulNormalClosure` `IsDomain.toNontrivial` `Ring.instIsDedekindDomainNormalClosure` `relNorm_eq_pow_of_isPrime_isGalois` `IsMaximal.isPrime'` `Ring.instIsGaloisFractionRingNormalClosure` `FractionRing.instFaithfulSMul` `IsGalois.tower_top_of_isGalois` `FractionRing.instIsScalarTower_1` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsDedekindDomain.toIsDomain` `UniqueFactorizationMonoid.instIsMulTorsionFree` `uniqueFactorizationMonoid` `Subsingleton.to_isMulTorsionFree` `Unique.instSubsingleton` `inertiaDeg_pos` `pow_mul` `inertiaDeg_algebra_tower` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `relNorm_relNorm`
`relNorm_eq_pow_of_isPrime_isGalois` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `inertiaDeg`	—	`FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Localization.isLocalization` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsIntegralClosure.of_isIntegrallyClosed` `Algebra.IsIntegral.of_finite` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `IsGalois.to_isSeparable` `IsGaloisGroup.of_isFractionRing` `instSMulDistribClassAlgEquiv` `IsGaloisGroup.of_isGalois` `inertiaDeg_pos` `eq_bot_of_liesOver_bot` `relNorm_bot` `bot_pow` `exists_relNorm_eq_pow_of_isPrime` `IsMaximal.isPrime'` `Set.mem_toFinset` `ramificationIdxIn_eq_ramificationIdx` `Finite.algEquiv` `Finite.algHom` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsDomain.to_noZeroDivisors` `instIsDomain` `instFiniteDimensionalFractionRingOfFinite` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `exists_smul_eq_of_isGaloisGroup` `relNorm_smul` `IsGaloisGroup.commutes` `pow_mul` `mul_comm` `map_algebraMap_eq_finset_prod_pow` `relNorm_algebraMap` `inertiaDegIn_eq_inertiaDeg` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `ramificationIdxIn_ne_zero` `primesOver_ncard_ne_zero` `IsLeftRegular.pow_injective` `UniqueFactorizationMonoid.instIsMulTorsionFree` `uniqueFactorizationMonoid` `Subsingleton.to_isMulTorsionFree` `Unique.instSubsingleton` `IsLeftCancelMulZero.mul_left_cancel_of_ne_zero` `isCancelMulZero` `one_eq_top` `IsMaximal.ne_top` `Set.ncard_eq_toFinset_card'` `ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn` `IsGaloisGroup.card_eq_finrank` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Finset.prod_congr` `map_pow` `Finset.prod_const`
`relNorm_int` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.instCommRing` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Int.instIsDomain` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Int.euclideanDomain` `Ring.toIntAlgebra` `CommRing.toRing` `Module.IsReflexive.to_isTorsionFree` `Int.instCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `span` `Int.instSemiring` `Set` `Set.instSingletonSet` `Nat.instMulZeroOneClass` `absNorm` `IsDomain.toNontrivial`	—	`Int.instIsDomain` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Module.IsReflexive.to_isTorsionFree` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `IsDomain.toNontrivial` `Int.instNontrivial` `Module.free_of_finite_type_torsion_free'` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `instIsTorsionFreeIntOfIsAddTorsionFree` `Int.instIsAddTorsionFree` `Int.ideal_span_absNorm_eq_self` `absNorm_relNorm` `PerfectField.ofCharZero` `IsFractionRing.charZero` `Int.instCharZero`
`relNorm_le_comap` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`spanNorm_le_comap`
`relNorm_map_algEquiv` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `IsDedekindDomain.toIsDomain` `map` `AlgEquiv` `AlgEquiv.instFunLike`	—	`le_antisymm` `IsDedekindDomain.toIsDomain` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_mapₐ` `AlgEquiv.symm_comp` `map_idₐ`
`relNorm_mono` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm`	—	`spanNorm_mono`
`relNorm_relNorm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `IsDedekindDomain.toIsDomain`	—	`spanNorm_spanNorm` `IsDedekindDomain.toIsDomain`
`relNorm_singleton` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `span` `Set` `Set.instSingletonSet` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing`	—	`spanNorm_singleton`
`relNorm_smul` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction`	—	`relNorm_map_algEquiv`
`relNorm_top` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`one_eq_top` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`spanIntNorm_localization` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`spanNorm` `map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Localization.isLocalization` `Submonoid.map_le_of_le_comap` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `LE.le.trans` `nonZeroDivisors_le_comap_nonZeroDivisors_of_injective` `IsDomain.to_noZeroDivisors` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `FractionRing.instFaithfulSMul` `IsScalarTower.of_algebraMap_eq'` `IsScalarTower.right` `RingHom.algebraMap_toAlgebra` `IsLocalization.map_comp` `RingHomCompTriple.comp_eq` `RingHomCompTriple.ids` `IsFractionRing.isFractionRing_of_isDomain_of_isLocalization` `IsLocalization.ringHom_ext` `RingHom.comp_assoc` `IsScalarTower.algebraMap_eq` `RingHom.comp_id` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `Algebra.IsIntegral.of_finite` `map_spanIntNorm` `Submodule.span_eq_span` `Set.image_subset_iff` `IsLocalization.mem_map_algebraMap_iff` `intNorm_mem_spanNorm` `pow_mem` `Submonoid.instSubmonoidClass` `map_pow` `IsFractionRing.injective` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Algebra.algebraMap_intNorm` `IsIntegralClosure.of_isIntegrallyClosed` `instFiniteDimensionalFractionRingOfFinite` `IsScalarTower.algebraMap_apply` `Algebra.norm_algebraMap` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Set.mem_preimage` `Algebra.intNorm_eq_of_isLocalization` `subset_span` `Set.mem_image_of_mem` `mem_map_of_mem`
`spanNorm_bot` 📖	mathematical	—	`spanNorm` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`span_eq_bot` `Set.image_singleton` `Algebra.intNorm_zero` `instFiniteDimensionalFractionRingOfFinite`
`spanNorm_eq` 📖	mathematical	—	`spanNorm` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `MonoidWithZeroHom.funLike` `relNorm`	—	—
`spanNorm_eq_bot_iff` 📖	mathematical	—	`spanNorm` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`instFiniteDimensionalFractionRingOfFinite` `eq_bot_iff` `instIsConcreteLE`
`spanNorm_le_comap` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `spanNorm` `comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `spanNorm.eq_1` `map.eq_1` `span_le` `Submodule.span_le` `Submodule.span_induction` `mem_comap` `mem_of_dvd` `Algebra.dvd_algebraMap_intNorm_self` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.add_mem` `Submodule.smul_mem`
`spanNorm_mono` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`spanNorm`	—	`span_mono` `Set.monotone_image`
`spanNorm_mul` 📖	mathematical	—	`spanNorm` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	—	`subsingleton_or_nontrivial` `IsScalarTower.right` `Unique.instSubsingleton` `spanNorm.congr_simp` `mul_top` `instIsTwoSided_1` `spanNorm_top` `eq_of_localization_maximal` `IsMaximal.isPrime'` `spanNorm_mul_of_bot_or_top` `IsMaximal.eq_of_le` `bot_le` `IsLocalization.isDomain_of_local_atPrime` `IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Localization.AtPrime.isDedekindDomain` `instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl` `instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` `Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain` `spanIntNorm_localization` `primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `OreLocalization.instIsScalarTower` `Localization.isLocalization` `map_mul` `RingHom.instRingHomClass` `IsScalarTower.left` `IsPrincipalIdealRing.principal` `instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal` `span_singleton_generator` `span_singleton_mul_span_singleton` `Algebra.IsIntegral.of_finite` `spanNorm_singleton` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`spanNorm_mul_of_bot_or_top` 📖	mathematical	`Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Top.top` `Submodule.instTop`	`spanNorm` `Submodule.mul` `IsScalarTower.right` `Algebra.id`	—	`le_antisymm` `IsScalarTower.right` `spanNorm_eq_bot_iff` `IsScalarTower.left` `bot_mul` `spanNorm_bot` `bot_le` `top_mul` `mul_bot` `le_refl` `le_top` `spanNorm_mul_spanNorm_le`
`spanNorm_mul_spanNorm_le` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `Algebra.id` `spanNorm`	—	`IsScalarTower.right` `spanNorm.eq_1` `map.eq_1` `IsScalarTower.left` `span_mul_span'` `instIsTwoSided_1` `Set.image_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `span_mono` `Set.monotone_image` `mul_mem_mul`
`spanNorm_singleton` 📖	mathematical	—	`spanNorm` `span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `Algebra.intNorm` `Algebra.IsIntegral.of_finite` `CommRing.toRing`	—	`le_antisymm` `Algebra.IsIntegral.of_finite` `span_le` `mem_span_singleton` `Set.mem_image` `map_dvd` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `span_singleton_le_iff_mem` `intNorm_mem_spanNorm` `mem_span_singleton_self`
`spanNorm_spanNorm` 📖	mathematical	—	`spanNorm`	—	`eq_of_localization_maximal` `IsMaximal.isPrime'` `spanNorm_spanNorm_of_bot_or_top` `IsMaximal.eq_of_le` `bot_le` `algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul` `IsDomain.to_noZeroDivisors` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `primeCompl_le_nonZeroDivisors` `IsLocalization.isDomain_of_local_atPrime` `IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Localization.AtPrime.isDedekindDomain` `instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl` `instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` `Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain` `spanIntNorm_localization` `instIsScalarTowerLocalizationAlgebraMapSubmonoid` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl` `instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2` `instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl` `instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization` `IsPrincipalIdealRing.principal` `instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal` `span_singleton_generator` `Algebra.IsIntegral.of_finite` `spanNorm_singleton` `instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl` `Algebra.intNorm_intNorm` `instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl`
`spanNorm_spanNorm_of_bot_or_top` 📖	mathematical	`Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Top.top` `Submodule.instTop`	`spanNorm`	—	`spanNorm_eq_bot_iff` `eq_top_iff_one` `le_spanNorm_spanNorm`
`spanNorm_top` 📖	mathematical	—	`spanNorm` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Algebra.IsIntegral.of_finite` `spanNorm.congr_simp` `spanNorm_singleton` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass`

---

← Back to Index