Documentation Verification Report

ToSquareZero

📁 Source: Mathlib/RingTheory/Derivation/ToSquareZero.lean

Statistics

Metric	Count
Definitions `derivationToSquareZeroEquivLift`, `derivationToSquareZeroOfLift`, `diffToIdealOfQuotientCompEq`, `liftOfDerivationToSquareZero`	4
Theorems `derivationToSquareZeroEquivLift_apply_coe_apply`, `derivationToSquareZeroEquivLift_symm_apply_apply_coe`, `derivationToSquareZeroOfLift_apply`, `diffToIdealOfQuotientCompEq_apply`, `liftOfDerivationToSquareZero_apply`, `liftOfDerivationToSquareZero_mk_apply`, `liftOfDerivationToSquareZero_mk_apply'`	7
Total	11

(root)

Definitions

Name	Category	Theorems
`derivationToSquareZeroEquivLift` 📖	CompOp	2 math math: `derivationToSquareZeroEquivLift_symm_apply_apply_coe`, `derivationToSquareZeroEquivLift_apply_coe_apply`
`derivationToSquareZeroOfLift` 📖	CompOp	1 math math: `derivationToSquareZeroOfLift_apply`
`diffToIdealOfQuotientCompEq` 📖	CompOp	1 math math: `diffToIdealOfQuotientCompEq_apply`
`liftOfDerivationToSquareZero` 📖	CompOp	2 math math: `liftOfDerivationToSquareZero_mk_apply`, `liftOfDerivationToSquareZero_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivationToSquareZeroEquivLift_apply_coe_apply` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `AlgHom.comp` `Ideal.Quotient.mkₐ` `IsScalarTower.toAlgHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Equiv` `Derivation` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `Ideal.Quotient.isScalarTower` `EquivLike.toFunLike` `Equiv.instEquivLike` `derivationToSquareZeroEquivLift` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Derivation.instFunLike` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `Ideal.Quotient.isScalarTower`
`derivationToSquareZeroEquivLift_symm_apply_apply_coe` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Submodule` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.restrictScalars` `Algebra.toSMul` `DFunLike.coe` `Derivation` `Submodule.addCommMonoid` `Submodule.module'` `IsScalarTower.right` `Derivation.instFunLike` `Equiv` `AlgHom` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `AlgHom.comp` `Ideal.Quotient.mkₐ` `IsScalarTower.toAlgHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Ideal.Quotient.isScalarTower` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `derivationToSquareZeroEquivLift` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ring.toAddCommGroup` `AlgHom.funLike` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `Ideal.Quotient.isScalarTower`
`derivationToSquareZeroOfLift_apply` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AlgHom.comp` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `Ideal.Quotient.mkₐ` `IsScalarTower.toAlgHom` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Ideal.Quotient.isScalarTower` `Algebra.toSMul`	`SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `Derivation` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toModule` `IsScalarTower.right` `Derivation.instFunLike` `derivationToSquareZeroOfLift` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AlgHom` `AlgHom.funLike` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.isScalarTower` `IsScalarTower.right`
`diffToIdealOfQuotientCompEq_apply` 📖	mathematical	`AlgHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.algebra` `Ideal.Quotient.mkₐ`	`CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap` `RingHom.id` `Submodule.addCommMonoid` `Algebra.toModule` `Submodule.module'` `Algebra.toSMul` `IsScalarTower.right` `LinearMap.instFunLike` `diffToIdealOfQuotientCompEq` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AlgHom` `AlgHom.funLike`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right`
`liftOfDerivationToSquareZero_apply` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `liftOfDerivationToSquareZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SetLike.instMembership` `Submodule.setLike` `Derivation` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Algebra.toModule` `Derivation.instFunLike` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.right`
`liftOfDerivationToSquareZero_mk_apply` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `AlgHom` `AlgHom.funLike` `liftOfDerivationToSquareZero` `Ideal.instHasQuotient_1` `Ideal.Quotient.semiring` `algebraMap` `Ideal.instAlgebraQuotient`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `liftOfDerivationToSquareZero_apply` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Ideal.Quotient.eq_zero_iff_mem` `Subtype.prop` `zero_add` `Ideal.Quotient.mk_algebraMap`
`liftOfDerivationToSquareZero_mk_apply'` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Derivation` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `Derivation.instFunLike` `Ideal.Quotient.semiring` `algebraMap` `Ideal.instAlgebraQuotient`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `Subtype.prop` `zero_add`

---

← Back to Index