Documentation Verification Report

RingHom

📁 Source: Mathlib/RingTheory/AdicCompletion/RingHom.lean

Statistics

Metric	Count
Definitions `liftRingHom`, `liftAlgHom`, `liftRingHom`	3
Theorems `eq_liftRingHom`, `factorPow_comp_eq_of_factorPow_comp_succ_eq'`, `mk_comp_liftRingHom`, `mk_liftRingHom`, `algHom_ext`, `eq_liftRingHom`, `mk_comp_liftRingHom`, `mk_liftAlgHom`, `mk_liftRingHom`, `mkₐ_comp_liftAlgHom`, `ofAlgEquiv_comp_liftRingHom`, `of_liftRingHom`	12
Total	15

IsAdicComplete

Definitions

Name	Category	Theorems
`liftAlgHom` 📖	CompOp	2 math math: `mk_liftAlgHom`, `mkₐ_comp_liftAlgHom`
`liftRingHom` 📖	CompOp	5 math math: `of_liftRingHom`, `ofAlgEquiv_comp_liftRingHom`, `mk_liftRingHom`, `eq_liftRingHom`, `mk_comp_liftRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`AlgHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `Ideal.Quotient.mkₐ`	—	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `AdicCompletion.instIsScalarTower` `AlgHom.cancel_left` `AlgEquiv.injective` `AlgHom.ext` `AdicCompletion.ext_evalₐ` `IsScalarTower.left` `AdicCompletion.ofAlgEquiv_apply` `AdicCompletion.evalₐ_of`
`eq_liftRingHom` 📖	mathematical	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsScalarTower.right` `Algebra.id`	`liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `DFunLike.coe_injective` `IsHausdorff.funext'` `toIsHausdorff` `mk_liftRingHom`
`mk_comp_liftRingHom` 📖	mathematical	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow`	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `RingHom.ext` `mk_liftRingHom`
`mk_liftAlgHom` 📖	mathematical	`AlgHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `Algebra.id` `Ideal.Quotient.algebra` `Ideal.Quotient.factorₐ` `Ideal.pow_le_pow_right`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `AlgHom` `AlgHom.funLike` `liftAlgHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.instIsTwoSided_1` `Ideal.pow_le_pow_right` `AdicCompletion.mk_ofAlgEquiv_symm` `AdicCompletion.evalₐ_liftAlgHom`
`mk_liftRingHom` 📖	mathematical	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `liftRingHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `AdicCompletion.evalₐ_of` `AdicCompletion.of_ofAlgEquiv_symm` `AdicCompletion.evalₐ_liftRingHom`
`mkₐ_comp_liftAlgHom` 📖	mathematical	`AlgHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `Algebra.id` `Ideal.Quotient.algebra` `Ideal.Quotient.factorₐ` `Ideal.pow_le_pow_right`	`AlgHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `Ideal.Quotient.mkₐ` `liftAlgHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.instIsTwoSided_1` `Ideal.pow_le_pow_right` `AlgHom.ext` `mk_liftAlgHom`
`ofAlgEquiv_comp_liftRingHom` 📖	mathematical	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow`	`RingHom.comp` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `AdicCompletion.instCommRing` `RingHomClass.toRingHom` `AlgEquiv` `Algebra.id` `AdicCompletion.instAlgebra` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `AdicCompletion.ofAlgEquiv` `liftRingHom` `AdicCompletion.liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `RingHom.ext` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AdicCompletion.ext` `AdicCompletion.ofAlgEquiv_apply` `of_liftRingHom`
`of_liftRingHom` 📖	mathematical	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AdicCompletion` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `AdicCompletion.instAddCommGroup` `AdicCompletion.instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `AdicCompletion.of` `RingHom` `RingHom.instFunLike` `liftRingHom` `AdicCompletion.instCommRing` `AdicCompletion.liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `AdicCompletion.of_ofAlgEquiv_symm`

IsAdicComplete.StrictMono

Definitions

Name	Category	Theorems
`liftRingHom` 📖	CompOp	3 math math: `mk_liftRingHom`, `eq_liftRingHom`, `mk_comp_liftRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_liftRingHom` 📖	mathematical	`StrictMono` `Nat.instPreorder` `RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `StrictMono.monotone` `Nat.instPartialOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsScalarTower.right` `Algebra.id`	`liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `StrictMono.monotone` `DFunLike.coe_injective` `IsHausdorff.StrictMono.funext'` `IsAdicComplete.toIsHausdorff` `mk_liftRingHom`
`factorPow_comp_eq_of_factorPow_comp_succ_eq'` 📖	mathematical	`StrictMono` `Nat.instPreorder` `RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `StrictMono.monotone` `Nat.instPartialOrder`	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `StrictMono.monotone` `Nat.instPartialOrder` `Nat.instPreorder`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `StrictMono.monotone` `RingHom.ext` `Submodule.eq_factor_of_eq_factor_succ` `Ideal.pow_le_pow_right`
`mk_comp_liftRingHom` 📖	mathematical	`StrictMono` `Nat.instPreorder` `RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `StrictMono.monotone` `Nat.instPartialOrder`	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `liftRingHom`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `StrictMono.monotone` `RingHom.ext` `mk_liftRingHom`
`mk_liftRingHom` 📖	mathematical	`StrictMono` `Nat.instPreorder` `RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factorPow` `StrictMono.monotone` `Nat.instPartialOrder`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `liftRingHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `StrictMono.monotone` `StrictMono.id_le` `instWellFoundedLTNat` `AdicCompletion.mk_ofAlgEquiv_symm` `AdicCompletion.evalₐ_liftRingHom` `factorPow_comp_eq_of_factorPow_comp_succ_eq'` `StrictMono.le_apply`

---

← Back to Index