Documentation Verification Report

LocalRing

📁 Source: Mathlib/RingTheory/Unramified/LocalRing.lean

Statistics

Metric	Count
Definitions	0
Theorems `iff_map_maximalIdeal_eq`, `isField_quotient_map_maximalIdeal`, `map_maximalIdeal`, `of_map_maximalIdeal`, `instFiniteResidueFieldOfFormallyUnramified`, `instFiniteResidueFieldOfIsUnramifiedAt`, `instFormallyUnramifiedResidueField`, `instFormallyUnramifiedResidueField_1`, `instIsSeparableResidueFieldOfFormallyUnramified`, `instIsSeparableResidueFieldOfIsUnramifiedAt`, `isUnramifiedAt_iff_map_eq`, `exists_awayMap_bijective_of_localRingHom_bijective`, `exists_awayMap_bijective_of_residueField_surjective`, `exists_awayMap_injective_of_localRingHom_injective`, `finite_of_primesOver_eq_singleton`, `localRingHom_injective_of_primesOver_eq_singleton`, `localRingHom_surjective_of_primesOver_eq_singleton`	17
Total	17

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteResidueFieldOfFormallyUnramified` 📖	mathematical	—	`Module.Finite` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `toModule` `Semifield.toCommSemiring` `IsLocalRing.ResidueField.instAlgebra`	—	`EssFiniteType.comp` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `EssFiniteType.of_finiteType` `Module.Finite.finiteType` `IsLocalRing.instFiniteResidueField` `Module.Finite.self` `EssFiniteType.of_comp` `IsLocalRing.ResidueField.instIsScalarTower` `IsScalarTower.left` `FormallyUnramified.finite_of_free` `instFormallyUnramifiedResidueField_1` `Module.Free.of_divisionRing`
`instFiniteResidueFieldOfIsUnramifiedAt` 📖	mathematical	—	`Module.Finite` `Ideal.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsLocalRing.instCommRingResidueField` `toModule` `Semifield.toCommSemiring` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`FormallyUnramified.finite_of_free` `instIsLocalHomAtPrimeRingHomAlgebraMap` `instFormallyUnramifiedResidueField_1` `instFormallyUnramifiedAtPrimeOfIsUnramifiedAt` `instEssFiniteTypeResidueField_1` `Module.Free.of_divisionRing`
`instFormallyUnramifiedResidueField` 📖	mathematical	—	`FormallyUnramified` `IsLocalRing.ResidueField` `IsLocalRing.instCommRingResidueField` `IsLocalRing.ResidueField.algebra` `id` `CommRing.toCommSemiring`	—	`FormallyUnramified.quotient` `FormallyUnramified.inst`
`instFormallyUnramifiedResidueField_1` 📖	mathematical	—	`FormallyUnramified` `IsLocalRing.ResidueField` `IsLocalRing.instCommRingResidueField` `IsLocalRing.ResidueField.instAlgebra`	—	`FormallyUnramified.comp` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `instFormallyUnramifiedResidueField` `FormallyUnramified.of_restrictScalars` `IsLocalRing.ResidueField.instIsScalarTower` `IsScalarTower.left`
`instIsSeparableResidueFieldOfFormallyUnramified` 📖	mathematical	—	`IsSeparable` `IsLocalRing.ResidueField` `IsLocalRing.instCommRingResidueField` `DivisionRing.toRing` `Field.toDivisionRing` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.instAlgebra`	—	`FormallyUnramified.isSeparable` `instFormallyUnramifiedResidueField_1` `EssFiniteType.of_finiteType` `Module.Finite.finiteType` `instFiniteResidueFieldOfFormallyUnramified`
`instIsSeparableResidueFieldOfIsUnramifiedAt` 📖	mathematical	—	`IsSeparable` `Ideal.ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionRing.toRing` `Field.toDivisionRing` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	—	`instIsLocalHomAtPrimeRingHomAlgebraMap` `Localization.AtPrime.isLocalRing` `isUnramifiedAt_iff_map_eq`
`isUnramifiedAt_iff_map_eq` 📖	mathematical	—	`IsUnramifiedAt` `IsSeparable` `Ideal.ResidueField` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionRing.toRing` `Field.toDivisionRing` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `RingHom.instFunLike` `algebraMap` `OreLocalization.instAlgebra` `IsLocalRing.maximalIdeal` `OreLocalization.instCommSemiring` `Localization.AtPrime.isLocalRing`	—	`EssFiniteType.of_comp` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `instEssFiniteTypeLocalization` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Localization.AtPrime.isLocalRing` `FormallyUnramified.of_restrictScalars` `FormallyUnramified.comp` `FormallyUnramified.instLocalization` `FormallyUnramified.inst` `FormallyUnramified.iff_map_maximalIdeal_eq` `RingHom.algebraMap_toAlgebra` `Localization.AtPrime.map_eq_maximalIdeal` `Ideal.map_map` `Localization.localRingHom.eq_1` `IsLocalization.map_comp` `IsScalarTower.algebraMap_eq` `OreLocalization.instIsScalarTower` `IsScalarTower.right`

Algebra.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_map_maximalIdeal_eq` 📖	mathematical	—	`Algebra.FormallyUnramified` `Algebra.IsSeparable` `IsLocalRing.ResidueField` `IsLocalRing.instCommRingResidueField` `DivisionRing.toRing` `Field.toDivisionRing` `IsLocalRing.ResidueField.field` `IsLocalRing.ResidueField.instAlgebra` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal`	—	`Algebra.instIsSeparableResidueFieldOfFormallyUnramified` `map_maximalIdeal` `of_map_maximalIdeal`
`isField_quotient_map_maximalIdeal` 📖	mathematical	—	`IsField` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal` `Ideal.Quotient.semiring`	—	`List.TFAE.out` `RingHom.instRingHomClass` `IsLocalRing.local_hom_TFAE` `IsScalarTower.right` `Ideal.Quotient.tower_quotient_map_quotient` `of_restrictScalars` `quotient` `Algebra.EssFiniteType.of_comp` `Algebra.instEssFiniteTypeQuotientIdeal` `finite_of_free` `Module.Free.of_divisionRing` `isReduced_of_field` `isArtinian_of_tower` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Ideal.Quotient.nontrivial_iff` `ne_top_of_le_ne_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal` `IsLocalRing.of_surjective'` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `IsLocalRing.jacobson_eq_maximalIdeal` `bot_ne_top` `Ideal.instNontrivial` `IsArtinianRing.jacobson_eq_radical` `Ideal.zero_eq_bot` `nilradical.eq_1` `nilradical_eq_zero` `IsLocalRing.isField_iff_maximalIdeal_eq`
`map_maximalIdeal` 📖	mathematical	—	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal`	—	`IsLocalRing.eq_maximalIdeal` `Ideal.Quotient.maximal_ideal_iff_isField_quotient` `isField_quotient_map_maximalIdeal`
`of_map_maximalIdeal` 📖	mathematical	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal`	`Algebra.FormallyUnramified`	—	`of_isSeparable` `comp` `IsLocalRing.ResidueField.instIsScalarTower` `IsScalarTower.left` `Algebra.instFormallyUnramifiedResidueField` `Algebra.to_smulCommClass` `IsLocalRing.subsingleton_tensorProduct` `KaehlerDifferential.finite` `RingHom.instRingHomClass` `IsLocalRing.instIsScalarTowerResidueField` `IsScalarTower.right` `KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange` `Ideal.Quotient.mk_surjective` `Ideal.instIsTwoSided_1` `subsingleton_kaehlerDifferential` `Ideal.toCotangent_surjective` `Submodule.span_induction` `smulCommClass_self` `Derivation.map_algebraMap` `TensorProduct.tmul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Derivation.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `TensorProduct.tmul_add` `add_zero` `IsLocalRing.residue_eq_zero_iff` `Derivation.leibniz` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `KaehlerDifferential.isScalarTower_of_tower` `smul_zero` `TensorProduct.zero_tmul`

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_awayMap_bijective_of_localRingHom_bijective` 📖	mathematical	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet` `Ideal.FG` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Function.Bijective` `AtPrime` `DFunLike.coe` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `localRingHom` `Ideal.over_def`	`SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Away` `Submonoid.powers` `CommMonoid.toMonoid` `awayMap`	—	`RingHom.instRingHomClass` `Ideal.over_def` `Algebra.FiniteType.out` `Module.Finite.finiteType` `isLocalization` `Function.Surjective.exists` `IsLocalization.mk'_surjective` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `le_comap_primeCompl_iff` `ge_of_eq` `localRingHom_mk'` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.eq_iff_exists` `Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton` `Algebra.IsIntegral.of_finite` `Ideal.IsPrime.mul_notMem` `exists_awayMap_injective_of_localRingHom_injective` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `prod_mem` `Dvd.dvd.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Algebra.map_top` `Subalgebra.map_le` `Algebra.adjoin_le_iff` `pow_one` `IsLocalization.mk'.congr_simp` `IsLocalization.map_mk'` `map_mul` `Finset.prod_erase_mul` `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.RingNF.nat_rawCast_1` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `IsLocalization.exists_mk'_eq` `pow_mem` `map_pow` `mk_eq_mk'` `one_pow` `map_one` `MonoidHomClass.toOneHomClass` `IsLocalization.smul_mk'`
`exists_awayMap_bijective_of_residueField_surjective` 📖	mathematical	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet` `Ideal.ResidueField` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.instAlgebra` `AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	`SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Function.Bijective` `Away` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `awayMap`	—	`instIsLocalHomAtPrimeRingHomAlgebraMap` `exists_awayMap_bijective_of_localRingHom_bijective` `RingHom.instRingHomClass` `FaithfulSMul.ker_algebraMap_eq_bot` `Submodule.fg_bot` `Ideal.over_def` `localRingHom_injective_of_primesOver_eq_singleton` `Algebra.IsIntegral.of_finite` `localRingHom_surjective_of_primesOver_eq_singleton`
`exists_awayMap_injective_of_localRingHom_injective` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `AtPrime` `DFunLike.coe` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `localRingHom` `Ideal.over_def`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Away` `Submonoid.powers` `CommMonoid.toMonoid` `awayMap`	—	`RingHom.instRingHomClass` `Ideal.over_def` `localRingHom_to_map` `Eq.le` `Ideal.subset_span` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.span_le` `IsLocalization.map_eq_zero_iff` `isLocalization` `pow_one` `Fintype.prod_eq_mul_prod_compl` `Submonoid.coe_mul` `mul_assoc` `mul_left_comm` `MulZeroClass.mul_zero` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `IsLocalization.exists_mk'_eq` `IsLocalization.map_mk'` `MonoidWithZeroHomClass.toMonoidHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.mk'_eq_zero_iff` `pow_add` `mul_pow`
`finite_of_primesOver_eq_singleton` 📖	mathematical	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet`	`Module.Finite` `AtPrime` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `AtPrime.instAlgebraOfLiesOver`	—	`Module.Finite.fg_top` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Finset.coe_image` `Submodule.span_span_of_tower` `AtPrime.instIsScalarTower` `IsScalarTower.left` `RingHomSurjective.ids` `Submodule.map_span` `Submodule.map_top` `LinearMap.coe_range` `AlgHom.coe_toLinearMap` `IsScalarTower.coe_toAlgHom'` `top_le_iff` `isLocalization` `IsLocalization.exists_mk'_eq` `Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton` `Algebra.IsIntegral.of_finite` `Submodule.smul_mem_iff_of_isUnit` `IsLocalization.map_units` `Algebra.smul_def` `IsScalarTower.algebraMap_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `mul_left_comm` `Submodule.subset_span`
`localRingHom_injective_of_primesOver_eq_singleton` 📖	mathematical	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet`	`AtPrime` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `localRingHom` `algebraMap` `Ideal.LiesOver.over` `Ideal.IsPrime` `Ideal.LiesOver` `Eq.ge` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	—	`Ideal.LiesOver.over` `Eq.ge` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `isLocalization` `IsLocalization.exists_mk'_eq` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `le_comap_primeCompl_iff` `ge_of_eq` `localRingHom_mk'` `Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton` `IsLocalization.mk'_eq_zero_iff` `FaithfulSMul.algebraMap_injective` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`localRingHom_surjective_of_primesOver_eq_singleton` 📖	mathematical	`Ideal.primesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Set` `Set.instSingletonSet` `Ideal.ResidueField` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.instAlgebra` `AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap`	`OreLocalization.instSemiring` `localRingHom` `Ideal.over_def`	—	`instIsLocalHomAtPrimeRingHomAlgebraMap` `finite_of_primesOver_eq_singleton` `Ideal.over_def` `RingHomSurjective.ids` `LinearMap.range_eq_top` `top_le_iff` `Submodule.le_of_le_smul_of_le_jacobson_bot` `AtPrime.isLocalRing` `Module.Finite.fg_top` `IsLocalRing.maximalIdeal_le_jacobson` `IsScalarTower.left` `IsScalarTower.right` `Ideal.smul_top_eq_map` `Algebra.FormallyUnramified.map_maximalIdeal` `Algebra.EssFiniteType.of_finiteType` `Module.Finite.finiteType` `Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt` `IsLocalRing.residue_surjective` `sub_sub_self` `sub_mem` `Submodule.addSubgroupClass` `Submodule.mem_sup_left` `Submodule.mem_sup_right` `IsLocalRing.residue_eq_zero_iff` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `IsLocalRing.ResidueField.algebraMap_eq` `IsScalarTower.algebraMap_apply` `IsLocalRing.instIsScalarTowerResidueField` `IsLocalRing.ResidueField.instIsScalarTower`

---

← Back to Index