Documentation Verification Report

LocalizationAway

📁 Source: Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean

Statistics

Metric	Count
Definitions `compLocalizationAwayAlgHom`, `cotangentCompAwaySec`, `cotangentCompLocalizationAwayEquiv`	3
Theorems `compLocalizationAwayAlgHom_X_inl`, `compLocalizationAwayAlgHom_relation_eq_zero`, `compLocalizationAwayAlgHom_toAlgHom_toComp`, `comp_localizationAway_ker`, `cotangentCompAwaySec_apply`, `cotangentCompLocalizationAwayEquiv_symm_comp_inl`, `cotangentCompLocalizationAwayEquiv_symm_inl`, `cotangentCompLocalizationAwayEquiv_symm_inr`, `liftBaseChange_injective_of_isLocalizationAway`, `map_comp_cotangentCompAwaySec`, `snd_comp_cotangentCompLocalizationAwayEquiv`, `snd_cotangentCompLocalizationAwayEquiv`, `sq_ker_comp_le_ker_compLocalizationAwayAlgHom`	13
Total	16

Algebra.Generators

Definitions

Name	Category	Theorems
`compLocalizationAwayAlgHom` 📖	CompOp	4 math math: `compLocalizationAwayAlgHom_toAlgHom_toComp`, `compLocalizationAwayAlgHom_X_inl`, `sq_ker_comp_le_ker_compLocalizationAwayAlgHom`, `compLocalizationAwayAlgHom_relation_eq_zero`
`cotangentCompAwaySec` 📖	CompOp	2 math math: `map_comp_cotangentCompAwaySec`, `cotangentCompAwaySec_apply`
`cotangentCompLocalizationAwayEquiv` 📖	CompOp	5 math math: `cotangentCompLocalizationAwayEquiv_symm_comp_inl`, `snd_comp_cotangentCompLocalizationAwayEquiv`, `snd_cotangentCompLocalizationAwayEquiv`, `cotangentCompLocalizationAwayEquiv_symm_inl`, `cotangentCompLocalizationAwayEquiv_symm_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLocalizationAwayAlgHom_X_inl` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Ring` `comp` `localizationAway` `Localization.Away` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ker` `CommRing.toCommMonoid` `Ideal.Quotient.commRing` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `σ` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MvPolynomial.algebra` `OreLocalization.instAlgebra` `Ideal.instAlgebraQuotient` `AlgHom.funLike` `compLocalizationAwayAlgHom` `MvPolynomial.X` `IsLocalization.Away.invSelf` `Ideal.Quotient.commSemiring` `OreLocalization.instCommSemiring` `Localization.isLocalization`	—	`Ideal.instIsTwoSided_1` `Localization.isLocalization` `MvPolynomial.aeval_X`
`compLocalizationAwayAlgHom_relation_eq_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Ring` `comp` `localizationAway` `Localization.Away` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ker` `CommRing.toCommMonoid` `Ideal.Quotient.commRing` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `σ` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MvPolynomial.algebra` `OreLocalization.instAlgebra` `Ideal.instAlgebraQuotient` `AlgHom.funLike` `compLocalizationAwayAlgHom` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.rename` `MvPolynomial.X` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `OreLocalization.instZero` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule` `Monoid.toMulAction`	—	`Ideal.instIsTwoSided_1` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `toComp_toAlgHom` `compLocalizationAwayAlgHom_toAlgHom_toComp` `Localization.isLocalization` `compLocalizationAwayAlgHom_X_inl` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.Away.mul_invSelf` `sub_self`
`compLocalizationAwayAlgHom_toAlgHom_toComp` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Ring` `comp` `localizationAway` `Localization.Away` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ker` `CommRing.toCommMonoid` `Ideal.Quotient.commRing` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `σ` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MvPolynomial.algebra` `OreLocalization.instAlgebra` `Ideal.instAlgebraQuotient` `AlgHom.funLike` `compLocalizationAwayAlgHom` `Hom.toAlgHom` `toComp` `algebraMap`	—	`Ideal.instIsTwoSided_1` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.Quotient.isScalarTower` `MvPolynomial.aeval_rename` `MvPolynomial.aeval_X_left_apply`
`comp_localizationAway_ker` 📖	mathematical	`DFunLike.coe` `RingHom` `Ring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `instRing`	`ker` `comp` `localizationAway` `Ideal` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.map` `AlgHom` `MvPolynomial.algebra` `AlgHom.funLike` `Hom.toAlgHom` `toComp` `Ideal.span` `Set` `Set.instSingletonSet` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.rename` `MvPolynomial.X` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Ideal.map_span` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Set.image_singleton` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `ker_localizationAway` `Hom.toAlgHom_X` `toAlgHom_ofComp_rename` `ofComp_val` `ker_comp_eq_sup` `map_toComp_ker` `Ideal.comap_map_of_surjective` `toAlgHom_ofComp_surjective` `RingHom.ker_eq_comap_bot` `sup_assoc` `sup_of_le_left`
`cotangentCompAwaySec_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `localizationAway` `comp` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `cotangentCompAwaySec` `cMulXSubOneCotangent`	—	`basisCotangentAway_apply` `cotangentCompAwaySec.eq_1` `RingHomInvPair.ids` `Module.Basis.constr_basis`
`cotangentCompLocalizationAwayEquiv_symm_comp_inl` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`LinearMap.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `TensorProduct.addCommMonoid` `Prod.instAddCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Prod.instModule` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `cotangentCompLocalizationAwayEquiv` `LinearMap.inl` `LinearMap.liftBaseChange` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toComp`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Cotangent.exact` `liftBaseChange_injective_of_isLocalizationAway` `map_comp_cotangentCompAwaySec`
`cotangentCompLocalizationAwayEquiv_symm_inl` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`LinearEquiv` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Prod.instAddCommMonoid` `TensorProduct.addCommMonoid` `Prod.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cotangentCompLocalizationAwayEquiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.liftBaseChange` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toComp`	—	`IsScalarTower.right` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.left` `RingHomCompTriple.ids` `cotangentCompLocalizationAwayEquiv_symm_comp_inl`
`cotangentCompLocalizationAwayEquiv_symm_inr` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`LinearEquiv` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Prod.instAddCommMonoid` `TensorProduct.addCommMonoid` `Prod.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cotangentCompLocalizationAwayEquiv` `TensorProduct.zero`	—	`IsScalarTower.right` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `zero_add` `cotangentCompAwaySec_apply`
`liftBaseChange_injective_of_isLocalizationAway` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `Algebra.Extension.Cotangent` `toExtension` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.toModule` `Algebra.Extension.instModuleCotangent` `Algebra.id` `comp` `localizationAway` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `LinearMap.liftBaseChange` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `Algebra.Extension.Cotangent.map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Hom.toExtensionHom` `toComp`	—	`Algebra.to_smulCommClass` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `IsScalarTower.left` `Ideal.instIsTwoSided_1` `IsLocalizedModule.injective_of_map_zero` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsLocalization.tensorProduct_isLocalizedModule` `IsScalarTower.to_smulCommClass` `Algebra.Extension.Cotangent.mk_surjective` `compLocalizationAwayAlgHom_toAlgHom_toComp` `sq_ker_comp_le_ker_compLocalizationAwayAlgHom` `one_smul` `IsLocalization.map_eq_zero_iff` `Localization.isLocalization` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `IsLocalizedModule.eq_zero_iff` `algebraMap_apply` `aeval_val_σ` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Algebra.Extension.Cotangent.mk_eq_zero_iff` `Ideal.Quotient.eq_zero_iff_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`map_comp_cotangentCompAwaySec` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`LinearMap.comp` `RingHomCompTriple.ids` `cotangentCompAwaySec` `LinearMap.id`	—	`IsScalarTower.right` `Module.Basis.ext` `RingHomCompTriple.ids` `basisCotangentAway_apply` `cotangentCompAwaySec_apply`
`snd_comp_cotangentCompLocalizationAwayEquiv` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`LinearMap.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Prod.instAddCommMonoid` `TensorProduct.addCommMonoid` `Prod.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.snd` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `cotangentCompLocalizationAwayEquiv`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.left` `Cotangent.exact` `liftBaseChange_injective_of_isLocalizationAway` `map_comp_cotangentCompAwaySec`
`snd_cotangentCompLocalizationAwayEquiv` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.Extension.Cotangent` `toExtension` `comp` `localizationAway` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `Algebra.Extension.Cotangent.map` `Hom.toExtensionHom` `IsScalarTower.right` `ofComp` `cMulXSubOneCotangent`	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `LinearEquiv` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `TensorProduct.addCommMonoid` `Prod.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `cotangentCompLocalizationAwayEquiv`	—	`IsScalarTower.right` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `snd_comp_cotangentCompLocalizationAwayEquiv`
`sq_ker_comp_le_ker_compLocalizationAwayAlgHom` 📖	mathematical	—	`Ideal` `Ring` `comp` `localizationAway` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ker` `RingHom.ker` `Localization.Away` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ideal.instHasQuotient` `CommRing.toCommMonoid` `Ideal.Quotient.commRing` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `σ` `AlgHom` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MvPolynomial.algebra` `OreLocalization.instAlgebra` `Ideal.instAlgebraQuotient` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `compLocalizationAwayAlgHom`	—	`Ideal.instIsTwoSided_1` `Ideal.mem_span_singleton` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `compLocalizationAwayAlgHom_relation_eq_zero` `MulZeroClass.zero_mul` `AlgHomClass.toRingHomClass` `comp_localizationAway_ker` `algebraMap_apply` `aeval_val_σ` `sq` `IsScalarTower.left` `Ideal.sup_mul` `Ideal.mul_sup` `sup_le` `IsScalarTower.right` `Ideal.map_mul` `Ideal.map_le_iff_le_comap` `compLocalizationAwayAlgHom_toAlgHom_toComp` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `Ideal.Quotient.algebraMap_eq` `Ideal.Quotient.eq_zero_iff_mem` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ideal.mul_le` `MulZeroClass.mul_zero`

---

← Back to Index