Documentation Verification Report

DualNumber

📁 Source: Mathlib/RingTheory/DualNumber.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_mul_left_or_mul_right`, `fst_eq_zero_iff_eps_dvd`, `ideal_trichotomy`, `instIsLocalRing`, `instIsPrincipalIdealRing`, `isMaximal_span_singleton_eps`, `isNilpotent_eps`, `isNilpotent_iff_eps_dvd`, `maximalIdeal_eq_span_singleton_eps`, `isNilpotent_iff_isNilpotent_fst`, `isNilpotent_inl_iff`, `isNilpotent_inr`, `isUnit_or_isNilpotent`, `isUnit_or_isNilpotent_of_isMaximal_isNilpotent`	14
Total	14

DualNumber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mul_left_or_mul_right` 📖	mathematical	—	`DualNumber` `TrivSqZeroExt.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Distrib.toAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `MulOpposite` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toOppositeModule`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `TrivSqZeroExt.isUnit_or_isNilpotent` `CanLift.prf` `instCanLiftUnitsValIsUnit` `Units.mul_inv_cancel_left` `isNilpotent_iff_eps_dvd` `eq_or_ne` `MulZeroClass.mul_zero` `TrivSqZeroExt.inl_mul` `mul_inv_cancel₀` `one_mul` `MulZeroClass.zero_mul` `zero_add`
`fst_eq_zero_iff_eps_dvd` 📖	mathematical	—	`TrivSqZeroExt.fst` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DualNumber` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `eps` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `MulZeroClass.zero_mul` `zero_smul` `zero_add` `one_mul`
`ideal_trichotomy` 📖	mathematical	—	`Bot.bot` `Ideal` `DualNumber` `TrivSqZeroExt.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Semiring.toModule` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `Submodule.instBot` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ideal.span` `Set` `Set.instSingletonSet` `eps` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Top.top` `Submodule.instTop`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `TrivSqZeroExt.isUnit_or_isNilpotent` `Ideal.eq_top_of_isUnit_mem` `isNilpotent_iff_eps_dvd` `TrivSqZeroExt.ext` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `one_mul` `zero_add` `mul_one` `Mathlib.Tactic.Contrapose.contrapose₄` `zero_smul` `inv_mul_cancel₀` `smul_neg` `neg_zero` `add_zero` `le_antisymm` `Commute.eq` `commute_eps_right` `Submodule.exists_mem_ne_zero_of_ne_bot` `commute_eps_left` `mul_assoc` `Ideal.mul_mem_left` `eq_or_ne`
`instIsLocalRing` 📖	mathematical	—	`IsLocalRing` `DualNumber` `TrivSqZeroExt.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Semiring.toModule` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `TrivSqZeroExt.instNontrivial_of_right` `Nontrivial.to_nonempty` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `eq_or_ne` `eq_sub_iff_add_eq` `add_comm` `sub_zero` `NeZero.one`
`instIsPrincipalIdealRing` 📖	mathematical	—	`IsPrincipalIdealRing` `DualNumber` `TrivSqZeroExt.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Semiring.toModule` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `ideal_trichotomy` `bot_isPrincipal` `top_isPrincipal`
`isMaximal_span_singleton_eps` 📖	mathematical	—	`Ideal.IsMaximal` `DualNumber` `TrivSqZeroExt.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Semiring.toModule` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `Ideal.span` `Set` `Set.instSingletonSet` `eps` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `MulZeroClass.mul_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mul_one` `zero_smul` `add_zero` `Nontrivial.to_nonempty` `TrivSqZeroExt.instNontrivial_of_right` `ideal_trichotomy`
`isNilpotent_eps` 📖	mathematical	—	`IsNilpotent` `DualNumber` `TrivSqZeroExt.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `MulOpposite` `MulOpposite.instSemiring` `Semiring.toOppositeModule` `eps` `AddMonoidWithOne.toOne`	—	`TrivSqZeroExt.isNilpotent_inr` `SMulCommClass.opposite_mid` `IsScalarTower.left`
`isNilpotent_iff_eps_dvd` 📖	mathematical	—	`IsNilpotent` `DualNumber` `TrivSqZeroExt.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `MulOpposite` `MulOpposite.instSemiring` `Semiring.toOppositeModule` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `TrivSqZeroExt.semiring` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsScalarTower.left` `DistribMulAction.toMulAction` `eps` `AddMonoidWithOne.toOne`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors`
`maximalIdeal_eq_span_singleton_eps` 📖	mathematical	—	`IsLocalRing.maximalIdeal` `DualNumber` `TrivSqZeroExt.commSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `instIsLocalRing` `Field.toDivisionRing` `Ideal.span` `Set` `Set.instSingletonSet` `eps` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`CommSemigroup.isCentralScalar` `instIsLocalRing` `IsLocalRing.eq_maximalIdeal` `isMaximal_span_singleton_eps`

TrivSqZeroExt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_iff_isNilpotent_fst` 📖	mathematical	—	`IsNilpotent` `TrivSqZeroExt` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instPowNatOfDistribMulActionMulOpposite` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite` `MulOpposite.instSemiring` `Monoid.toNatPow` `fst`	—	`fst_pow` `fst_zero` `pow_mul` `ext` `zero_pow` `two_ne_zero` `pow_two` `snd_mul` `MulOpposite.op_zero` `zero_smul` `zero_add` `snd_zero`
`isNilpotent_inl_iff` 📖	mathematical	—	`IsNilpotent` `TrivSqZeroExt` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instPowNatOfDistribMulActionMulOpposite` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite` `MulOpposite.instSemiring` `inl` `Monoid.toNatPow`	—	`isNilpotent_iff_isNilpotent_fst` `fst_inl`
`isNilpotent_inr` 📖	mathematical	—	`IsNilpotent` `TrivSqZeroExt` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instPowNatOfDistribMulActionMulOpposite` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite` `MulOpposite.instSemiring` `inr`	—	`pow_two` `inr_mul_inr`
`isUnit_or_isNilpotent` 📖	mathematical	—	`IsUnit` `TrivSqZeroExt` `monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `MulOpposite` `MulOpposite.instSemiring` `IsNilpotent` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instPowNatOfDistribMulActionMulOpposite`	—	`isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors`
`isUnit_or_isNilpotent_of_isMaximal_isNilpotent` 📖	mathematical	`IsNilpotent` `Ideal` `CommSemiring.toSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`IsUnit` `TrivSqZeroExt` `monoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `MulOpposite` `MulOpposite.instSemiring` `IsScalarTower.to_smulCommClass` `MulOpposite.instAlgebra` `IsScalarTower.op_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.toSMul` `IsScalarTower.left` `DistribMulAction.toMulAction` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instPowNatOfDistribMulActionMulOpposite`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass` `IsScalarTower.op_right` `IsScalarTower.left` `isUnit_iff_isUnit_fst` `isNilpotent_iff_isNilpotent_fst` `exists_max_ideal_of_mem_nonunits` `mem_nonunits_iff` `Eq.le` `Ideal.pow_mem_pow` `em`

---

← Back to Index