Documentation Verification Report

Hom

📁 Source: Mathlib/Algebra/Group/Units/Hom.lean

Statistics

Metric	Count
Definitions `toHomAddUnits`, `coeHom`, `liftRight`, `map`, `Hom`, `Hom`, `liftRight`, `IsLocalHom`, `liftRight`, `toHomUnits`, `toHomUnitsMulEquiv`, `coeHom`, `liftRight`, `map`	14
Theorems `coe_toHomAddUnits`, `add_liftRight_neg`, `coeHom_apply`, `coeHom_injective`, `coe_liftRight`, `coe_map`, `coe_map_neg`, `liftRight_neg_add`, `map_bijective`, `map_comp`, `map_id`, `map_injective`, `map_mk`, `val_zsmul_eq_zsmul_val`, `addUnit_map`, `addUnit_neg_map`, `add_liftRight_neg`, `coe_liftRight`, `eq_on_neg`, `liftRight_neg_add`, `map`, `of_leftInverse`, `map_nonunit`, `coe_liftRight`, `eq_on_inv`, `liftRight_inv_mul`, `map`, `mul_liftRight_inv`, `of_leftInverse`, `of_map`, `unit_inv_map`, `unit_map`, `coe_toHomUnits`, `isLocalHom_comp`, `isLocalHom_of_comp`, `toHomUnitsMulEquiv_apply`, `toHomUnitsMulEquiv_symm_apply`, `toHomUnits_mul`, `coeHom_apply`, `coeHom_injective`, `coe_liftRight`, `coe_map`, `coe_map_inv`, `liftRight_inv_mul`, `map_bijective`, `map_comp`, `map_id`, `map_injective`, `map_mk`, `mul_liftRight_inv`, `val_zpow_eq_zpow_val`, `eq_on_inv`, `eq_on_neg`, `isAddUnit_map_of_leftInverse`, `isLocalHom_of_leftInverse`, `isLocalHom_toMonoidHom`, `isUnit_map_iff`, `isUnit_map_of_leftInverse`, `isUnit_of_map_unit`, `map_addUnits_neg`, `map_units_inv`	61
Total	75

AddMonoidHom

Definitions

Name	Category	Theorems
`toHomAddUnits` 📖	CompOp	2 math math: `ker_toHomAddUnits`, `coe_toHomAddUnits`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHomAddUnits` 📖	mathematical	—	`AddUnits.val` `DFunLike.coe` `AddMonoidHom` `AddUnits` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddUnits.instAddZeroClass` `instFunLike` `toHomAddUnits`	—	—

AddUnits

Definitions

Name	Category	Theorems
`coeHom` 📖	CompOp	4 math math: `coeHom_apply`, `AddSubmonoid.mk_add_mk_neg_eq_zero`, `coeHom_injective`, `AddSubmonoid.mk_neg_add_mk_eq_zero`
`liftRight` 📖	CompOp	3 math math: `add_liftRight_neg`, `liftRight_neg_add`, `coe_liftRight`
`map` 📖	CompOp	10 math math: `map_mk`, `Continuous.addUnits_map`, `map_bijective`, `coe_map_neg`, `coe_map`, `map_injective`, `isOpenMap_map`, `map_id`, `continuous_map`, `map_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_liftRight_neg` 📖	mathematical	`val` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `AddUnits` `instNeg` `instAddZeroClass` `liftRight` `AddZero.toZero`	—	`add_neg_eq_iff_eq_add` `zero_add` `coe_liftRight`
`coeHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddUnits` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `coeHom` `val`	—	—
`coeHom_injective` 📖	mathematical	—	`AddUnits` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `coeHom`	—	`val_injective`
`coe_liftRight` 📖	mathematical	`val` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddUnits` `instAddZeroClass` `liftRight`	—	—
`coe_map` 📖	mathematical	—	`val` `DFunLike.coe` `AddMonoidHom` `AddUnits` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `map` `AddMonoid.toAddZeroClass`	—	—
`coe_map_neg` 📖	mathematical	—	`val` `AddUnits` `instNeg` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `map` `AddMonoid.toAddZeroClass`	—	—
`liftRight_neg_add` 📖	mathematical	`val` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `AddUnits` `instNeg` `instAddZeroClass` `liftRight` `AddZero.toZero`	—	`neg_add_eq_iff_eq_add` `add_zero` `coe_liftRight`
`map_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddUnits` `instAddZeroClass` `map`	—	`map_injective` `Function.Bijective.injective` `Function.Bijective.surjective` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`map_comp` 📖	mathematical	—	`map` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits` `instAddZeroClass`	—	—
`map_id` 📖	mathematical	—	`map` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits` `instAddZeroClass`	—	`AddMonoidHom.ext` `ext`
`map_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddUnits` `instAddZeroClass` `map`	—	`ext`
`map_mk` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`DFunLike.coe` `AddMonoidHom` `AddUnits` `instAddZeroClass` `AddMonoidHom.instFunLike` `map`	—	—
`val_zsmul_eq_zsmul_val` 📖	mathematical	—	`val` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `AddUnits` `SubNegMonoid.toZSMul` `instSubNegAddMonoid`	—	`AddMonoidHom.map_zsmul`

Algebra.Extension

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

Algebra.Generators

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	2 math math: `Hom.equivAlgHom_symm_apply_val`, `Hom.equivAlgHom_apply_coe`

IsAddUnit

Definitions

Name	Category	Theorems
`liftRight` 📖	CompOp	9 math math: `AddSubmonoid.LocalizationMap.add_neg_right`, `add_liftRight_neg`, `AddSubmonoid.LocalizationMap.lift_apply`, `AddSubmonoid.LocalizationMap.add_neg`, `AddSubmonoid.LocalizationMap.neg_unique`, `coe_liftRight`, `liftRight_neg_add`, `AddSubmonoid.LocalizationMap.lift_mk'`, `AddSubmonoid.LocalizationMap.add_neg_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addUnit_map` 📖	mathematical	`IsAddUnit`	`AddUnits.val` `addUnit` `DFunLike.coe` `map`	—	`map`
`addUnit_neg_map` 📖	mathematical	`IsAddUnit`	`AddUnits.val` `AddUnits` `AddUnits.instNeg` `addUnit` `DFunLike.coe` `map`	—	`AddUnits.neg_eq_of_add_eq_zero_left` `map` `map_add` `AddMonoidHomClass.toAddHomClass` `val_neg_add` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`add_liftRight_neg` 📖	mathematical	`IsAddUnit` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `AddUnits.instAddZeroClass` `liftRight` `AddZero.toZero`	—	`AddUnits.add_liftRight_neg`
`coe_liftRight` 📖	mathematical	`IsAddUnit` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddUnits.val` `AddUnits` `AddUnits.instAddZeroClass` `liftRight`	—	—
`eq_on_neg` 📖	mathematical	`IsAddUnit` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `DFunLike.coe`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`left_neg_eq_right_neg` `map_add_eq_zero` `neg_add_cancel` `add_neg_cancel`
`liftRight_neg_add` 📖	mathematical	`IsAddUnit` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `AddUnits.instAddZeroClass` `liftRight` `AddZero.toZero`	—	`AddUnits.liftRight_neg_add`
`map` 📖	mathematical	`IsAddUnit`	`DFunLike.coe`	—	`AddUnits.isAddUnit`
`of_leftInverse` 📖	—	`DFunLike.coe` `IsAddUnit`	—	—	`map`

IsLocalHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_nonunit` 📖	—	`IsUnit` `DFunLike.coe`	—	—	—

IsUnit

Definitions

Name	Category	Theorems
`liftRight` 📖	CompOp	12 math math: `IsLocalization.mul_add_inv_left`, `Submonoid.LocalizationMap.inv_unique`, `IsLocalization.lift_mk'`, `coe_liftRight`, `mul_liftRight_inv`, `Submonoid.LocalizationMap.lift_mk'`, `Submonoid.LocalizationMap.lift_apply`, `Submonoid.LocalizationMap.mul_inv_right`, `Submonoid.LocalizationMap.mul_inv_left`, `Submonoid.LocalizationMap.mul_inv`, `Submonoid.LocalizationMap.lift₀_apply`, `liftRight_inv_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_liftRight` 📖	mathematical	`IsUnit` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Units.val` `Units` `Units.instMulOneClass` `liftRight`	—	—
`eq_on_inv` 📖	mathematical	`IsUnit` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DFunLike.coe`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`left_inv_eq_right_inv` `map_mul_eq_one` `inv_mul_cancel` `mul_inv_cancel`
`liftRight_inv_mul` 📖	mathematical	`IsUnit` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`MulOne.toMul` `Units.val` `Units` `Units.instInv` `Units.instMulOneClass` `liftRight` `MulOne.toOne`	—	`Units.liftRight_inv_mul`
`map` 📖	mathematical	`IsUnit`	`DFunLike.coe`	—	`Units.isUnit`
`mul_liftRight_inv` 📖	mathematical	`IsUnit` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`MulOne.toMul` `Units.val` `Units` `Units.instInv` `Units.instMulOneClass` `liftRight` `MulOne.toOne`	—	`Units.mul_liftRight_inv`
`of_leftInverse` 📖	—	`DFunLike.coe` `IsUnit`	—	—	`map`
`of_map` 📖	—	`IsUnit` `DFunLike.coe`	—	—	`IsLocalHom.map_nonunit`
`unit_inv_map` 📖	mathematical	`IsUnit`	`Units.val` `Units` `Units.instInv` `unit` `DFunLike.coe` `map`	—	`Units.inv_eq_of_mul_eq_one_left` `map` `MonoidHomClass.toMulHomClass` `val_inv_mul` `map_one` `MonoidHomClass.toOneHomClass`
`unit_map` 📖	mathematical	`IsUnit`	`Units.val` `unit` `DFunLike.coe` `map`	—	`map`

MonoidHom

Definitions

Name	Category	Theorems
`toHomUnits` 📖	CompOp	5 math math: `toHomPerm_apply_symm_apply`, `ker_toHomUnits`, `coe_toHomUnits`, `toHomUnits_mul`, `toHomUnitsMulEquiv_apply`
`toHomUnitsMulEquiv` 📖	CompOp	2 math math: `toHomUnitsMulEquiv_symm_apply`, `toHomUnitsMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHomUnits` 📖	mathematical	—	`Units.val` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMulOneClass` `instFunLike` `toHomUnits`	—	—
`isLocalHom_comp` 📖	mathematical	—	`IsLocalHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike` `comp`	—	`IsLocalHom.map_nonunit`
`isLocalHom_of_comp` 📖	mathematical	—	`IsLocalHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	`isUnit_map_iff` `instMonoidHomClass` `IsUnit.map`
`toHomUnitsMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommMonoid.toMonoid` `Units` `Units.instMulOneClass` `mul` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toHomUnitsMulEquiv` `toHomUnits`	—	—
`toHomUnitsMulEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `Units` `CommMonoid.toMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMulOneClass` `mul` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toHomUnitsMulEquiv` `comp` `Units.coeHom`	—	—
`toHomUnits_mul` 📖	mathematical	—	`toHomUnits` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `mul` `Units` `Units.instMulOneClass` `CommGroup.toCommMonoid` `Units.instCommGroupUnits`	—	`ext` `Units.ext`

Units

Definitions

Name	Category	Theorems
`coeHom` 📖	CompOp	10 math math: `Submonoid.mk_mul_mk_inv_eq_one`, `Submonoid.mk_inv_mul_mk_eq_one`, `unitary_eq`, `WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv`, `pinGroup.mem_lipschitzGroup`, `pinGroup.mem_iff`, `coeHom_apply`, `lipschitzGroup.coe_mem_iff_mem`, `MonoidHom.toHomUnitsMulEquiv_symm_apply`, `coeHom_injective`
`liftRight` 📖	CompOp	3 math math: `coe_liftRight`, `mul_liftRight_inv`, `liftRight_inv_mul`
`map` 📖	CompOp	45 math math: `ValuationSubring.coe_mem_principalUnitGroup_iff`, `Matrix.GeneralLinearGroup.map_det`, `unitsNonZeroDivisorsEquiv_apply`, `Submodule.ker_unitsToPic`, `LinearEquiv.det_baseChange`, `Valuation.unit_map_eq`, `coe_map`, `map_mk`, `map_bijective`, `AffineEquiv.linear_equivUnitsAffineMap_symm_apply`, `map_neg`, `map_injective`, `unitary.toUnits_comp_map`, `coe_map_inv`, `isOpenMap_map`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq`, `map_id`, `Submodule.unitsQuotEquivRelPic_symm_apply`, `PowerSeries.map_invUnitsSub`, `Algebra.smul_units_def`, `Unitary.toUnits_comp_map`, `ClassGroup.equivPic_symm_apply`, `Continuous.units_map`, `IsLocalRing.surjective_units_map_of_local_ringHom`, `ValuationSubring.principalUnitGroupEquiv_apply`, `map_comp`, `FiniteField.unitsMap_norm_surjective`, `AlgEquiv.smul_units_def`, `continuous_map`, `WeierstrassCurve.map_Δ'`, `FractionalIdeal.map_canonicalEquiv_mk0`, `Submodule.mulExact_unitsMap_spanSingleton_unitsToPic`, `WeierstrassCurve.inv_map_Δ'`, `ClassGroup.mk_canonicalEquiv`, `ClassGroup.equivPic_apply`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq`, `mapContinuousMulEquiv_apply`, `ClassGroup.mk_def`, `WeierstrassCurve.VariableChange.map_u`, `Submodule.ker_unitsMap_spanSingleton`, `map_neg_one`, `ValuationSubring.principalUnitGroup_symm_apply`, `Submodule.unitsQuotEquivRelPic_apply_coe`, `IsPrimitiveRoot.map_rootsOfUnity`, `ZMod.unitsMap_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `instMulOneClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `coeHom` `val`	—	—
`coeHom_injective` 📖	mathematical	—	`Units` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `coeHom`	—	`val_injective`
`coe_liftRight` 📖	mathematical	`val` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Units` `instMulOneClass` `liftRight`	—	—
`coe_map` 📖	mathematical	—	`val` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `map` `Monoid.toMulOneClass`	—	—
`coe_map_inv` 📖	mathematical	—	`val` `Units` `instInv` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `map` `Monoid.toMulOneClass`	—	—
`liftRight_inv_mul` 📖	mathematical	`val` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`MulOne.toMul` `Units` `instInv` `instMulOneClass` `liftRight` `MulOne.toOne`	—	`inv_mul_eq_iff_eq_mul` `mul_one` `coe_liftRight`
`map_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Units` `instMulOneClass` `map`	—	`map_injective` `Function.Bijective.injective` `Function.Bijective.surjective` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass`
`map_comp` 📖	mathematical	—	`map` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units` `instMulOneClass`	—	—
`map_id` 📖	mathematical	—	`map` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units` `instMulOneClass`	—	`MonoidHom.ext` `ext`
`map_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Units` `instMulOneClass` `map`	—	`ext`
`map_mk` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`DFunLike.coe` `MonoidHom` `Units` `instMulOneClass` `MonoidHom.instFunLike` `map`	—	—
`mul_liftRight_inv` 📖	mathematical	`val` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`MulOne.toMul` `Units` `instInv` `instMulOneClass` `liftRight` `MulOne.toOne`	—	`mul_inv_eq_iff_eq_mul` `one_mul` `coe_liftRight`
`val_zpow_eq_zpow_val` 📖	mathematical	—	`val` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `Units` `DivInvMonoid.toZPow` `instDivInvMonoid`	—	`MonoidHom.map_zpow`

(root)

Definitions

Name	Category	Theorems
`IsLocalHom` 📖	CompData	66 math math: `ExteriorAlgebra.isLocalHom_algebraMap`, `MonoidAlgebra.isLocalHom_algebraMap`, `Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap`, `IsLocalRing.instIsLocalHomRingHomOfNontrivial`, `instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial`, `AlgebraicGeometry.ValuativeCriterion.Existence.instIsLocalHomCarrierRingHomHomHomCommRingCat`, `AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe`, `instIsLocalHomAtPrimeRingHomAlgebraMap`, `IsLocalRing.instIsLocalHomResidueFieldRingHomResidue`, `IsLocalHom.of_surjective`, `isLocalHom_toMonoidHom`, `RingHom.IsIntegral.isLocalHom`, `AddMonoidAlgebra.isLocalHom_singleZeroRingHom`, `AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap`, `AddMonoidAlgebra.isLocalHom_algebraMap`, `MonoidAlgebra.isLocalHom_singleOneRingHom`, `CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι`, `isLocalHom_equiv`, `MvPolynomial.instIsLocalHomRingHomAlgebraMap`, `isLocalHom_of_comp`, `MonoidHom.isLocalHom_comp`, `MonoidAlgebra.isLocalHom_singleOneAlgHom`, `RingHom.isLocalHom_comp`, `AlgebraicGeometry.LocallyRingedSpace.Hom.prop`, `AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst`, `AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom`, `IsLocalRing.exists_factor_valuationRing`, `isLocalHom_id`, `IsLocalHom.of_specComap_surjective`, `Valuation.HasExtension.instIsLocalHomValuationInteger`, `MvPolynomial.isLocalHom_expand`, `AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom`, `Polynomial.instIsLocalHomRingHomC`, `AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap'`, `isLocalHom_of_isIso`, `CommRingCat.equalizer_ι_isLocalHom'`, `AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo'`, `IsLocalRing.isLocalHom_iff_comap_closedPoint`, `MvPowerSeries.map.isLocalHom`, `IsLocalRing.isLocalHom_residue`, `CommRingCat.equalizer_ι_isLocalHom`, `isLocalHom_of_le_jacobson_bot`, `LocalSubring.le_def`, `AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply`, `Function.Surjective.isLocalHom`, `isLocalHom_of_iso`, `Localization.isLocalHom_localRingHom`, `CommRingCat.isLocalHom_comp`, `instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial`, `isLocalHom_of_exists_map_ne_one`, `AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo`, `isLocalHom_of_leftInverse`, `AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff`, `Algebra.IsIntegral.isLocalHom`, `AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr`, `Polynomial.isLocalHom_expand`, `AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap`, `isLocalHom_toRingHom`, `IsLocalRing.local_hom_TFAE`, `AddMonoidAlgebra.isLocalHom_singleZeroAlgHom`, `AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap`, `MvPolynomial.instIsLocalHomRingHomC`, `Polynomial.instIsLocalHomRingHomAlgebraMap`, `PowerSeries.map.isLocalHom`, `IsLocalHom.of_comap_surjective`, `MonoidHom.isLocalHom_of_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_on_inv` 📖	mathematical	`DFunLike.coe`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`IsUnit.eq_on_inv` `Group.isUnit`
`eq_on_neg` 📖	mathematical	`DFunLike.coe`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsAddUnit.eq_on_neg` `AddGroup.isAddUnit`
`isAddUnit_map_of_leftInverse` 📖	mathematical	`DFunLike.coe`	`IsAddUnit`	—	`IsAddUnit.of_leftInverse` `IsAddUnit.map`
`isLocalHom_of_leftInverse` 📖	mathematical	`DFunLike.coe`	`IsLocalHom`	—	`isUnit_map_of_leftInverse`
`isLocalHom_toMonoidHom` 📖	mathematical	—	`IsLocalHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `MonoidHomClass.toMonoidHom`	—	`IsLocalHom.map_nonunit`
`isUnit_map_iff` 📖	mathematical	—	`IsUnit` `DFunLike.coe`	—	`IsLocalHom.map_nonunit` `IsUnit.map`
`isUnit_map_of_leftInverse` 📖	mathematical	`DFunLike.coe`	`IsUnit`	—	`IsUnit.of_leftInverse` `IsUnit.map`
`isUnit_of_map_unit` 📖	—	`IsUnit` `DFunLike.coe`	—	—	`IsUnit.of_map`
`map_addUnits_neg` 📖	mathematical	—	`DFunLike.coe` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`AddMonoidHom.map_neg`
`map_units_inv` 📖	mathematical	—	`DFunLike.coe` `Units.val` `Units` `Units.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`MonoidHom.map_inv`

---

← Back to Index