Documentation Verification Report

Ext

📁 Source: Mathlib/Algebra/Ring/Ext.lean

Statistics

Metric	Count
Definitions	0
Theorems `ext`, `ext_iff`, `ext`, `ext_iff`, `toAddMonoidWithOne_injective`, `ext`, `ext_iff`, `ext`, `ext_iff`, `ext`, `ext_iff`, `toRing_injective`, `ext`, `ext_iff`, `toSemiring_injective`, `ext`, `ext_iff`, `ext`, `ext_iff`, `toNonAssocSemiring_injective`, `toNonUnitalNonAssocring_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocSemiring_injective`, `ext`, `ext_iff`, `toNonUnitalRing_injective`, `ext`, `ext_iff`, `toNonUnitalSemiring_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocRing_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocSemiring_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocSemiring_injective`, `ext`, `ext_iff`, `toDistrib_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocring_injective`, `toNonUnitalSemiring_injective`, `ext`, `ext_iff`, `toNonUnitalNonAssocSemiring_injective`, `ext`, `ext_iff`, `toNonAssocRing_injective`, `toNonUnitalRing_injective`, `toSemiring_injective`, `ext`, `ext_iff`, `toNonAssocSemiring_injective`, `toNonUnitalSemiring_injective`	58
Total	58

AddCommGroupWithOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommMonoidWithOne.toAddCommMonoid` `toAddCommMonoidWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `toAddGroupWithOne`	—	—	`AddCommGroup.ext` `AddGroupWithOne.ext` `natCast_zero` `natCast_succ` `SubNegMonoid.sub_eq_add_neg` `SubNegMonoid.zsmul_zero'` `SubNegMonoid.zsmul_succ'` `SubNegMonoid.zsmul_neg'` `AddGroup.neg_add_cancel` `intCast_ofNat` `intCast_negSucc`
`ext_iff` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommMonoidWithOne.toAddCommMonoid` `toAddCommMonoidWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `toAddGroupWithOne`	—	`ext`

AddCommMonoidWithOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `AddMonoidWithOne.toOne` `toAddMonoidWithOne`	—	—	`toAddMonoidWithOne_injective` `AddMonoidWithOne.ext`
`ext_iff` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `AddMonoidWithOne.toOne` `toAddMonoidWithOne`	—	`ext`
`toAddMonoidWithOne_injective` 📖	mathematical	—	`AddCommMonoidWithOne` `AddMonoidWithOne` `toAddMonoidWithOne`	—	—

AddGroupWithOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `toAddMonoidWithOne` `AddMonoidWithOne.toOne`	—	—	`AddMonoidWithOne.ext` `AddGroup.ext` `sub_eq_add_neg` `zsmul_zero'` `zsmul_succ'` `zsmul_neg'` `neg_add_cancel` `intCast_ofNat` `intCast_negSucc`
`ext_iff` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `toAddMonoidWithOne` `AddMonoidWithOne.toOne`	—	`ext`

AddMonoidWithOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toAddMonoid` `toOne`	—	—	`AddMonoid.ext` `natCast_zero` `natCast_succ`
`ext_iff` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toAddMonoid` `toOne`	—	`ext`

CommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `toNonUnitalCommRing` `Distrib.toMul`	—	—	`toRing_injective` `Ring.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `toNonUnitalCommRing` `Distrib.toMul`	—	`ext`
`toRing_injective` 📖	mathematical	—	`CommRing` `Ring` `toRing`	—	—

CommSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `Distrib.toMul`	—	—	`toSemiring_injective` `Semiring.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `Distrib.toMul`	—	`ext`
`toSemiring_injective` 📖	mathematical	—	`CommSemiring` `Semiring` `toSemiring`	—	—

Distrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toAdd` `toMul`	—	—	—
`ext_iff` 📖	mathematical	—	`toAdd` `toMul`	—	`ext`

NonAssocRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	—	`NonUnitalNonAssocRing.ext` `NonAssocSemiring.ext` `AddCommGroupWithOne.ext` `AddCommGroup.add_comm` `NonUnitalNonAssocRing.left_distrib` `NonUnitalNonAssocRing.right_distrib` `NonUnitalNonAssocRing.zero_mul` `NonUnitalNonAssocRing.mul_zero` `one_mul` `mul_one` `natCast_zero` `natCast_succ` `intCast_ofNat` `intCast_negSucc`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	`ext`
`toNonAssocSemiring_injective` 📖	mathematical	—	`NonAssocRing` `NonAssocSemiring` `toNonAssocSemiring`	—	`ext`
`toNonUnitalNonAssocring_injective` 📖	mathematical	—	`NonAssocRing` `NonUnitalNonAssocRing` `toNonUnitalNonAssocRing`	—	`ext`

NonAssocSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	—	`NonUnitalNonAssocSemiring.ext` `MulOneClass.ext` `AddCommMonoidWithOne.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocSemiring_injective` 📖	mathematical	—	`NonAssocSemiring` `NonUnitalNonAssocSemiring` `toNonUnitalNonAssocSemiring`	—	`ext`

NonUnitalCommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `toNonUnitalNonAssocCommRing` `Distrib.toMul`	—	—	`toNonUnitalRing_injective` `NonUnitalRing.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `toNonUnitalNonAssocCommRing` `Distrib.toMul`	—	`ext`
`toNonUnitalRing_injective` 📖	mathematical	—	`NonUnitalCommRing` `NonUnitalRing` `toNonUnitalRing`	—	—

NonUnitalCommSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `toNonUnitalSemiring` `Distrib.toMul`	—	—	`toNonUnitalSemiring_injective` `NonUnitalSemiring.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `toNonUnitalSemiring` `Distrib.toMul`	—	`ext`
`toNonUnitalSemiring_injective` 📖	mathematical	—	`NonUnitalCommSemiring` `NonUnitalSemiring` `toNonUnitalSemiring`	—	—

NonUnitalNonAssocCommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	—	`toNonUnitalNonAssocRing_injective` `NonUnitalNonAssocRing.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocRing_injective` 📖	mathematical	—	`NonUnitalNonAssocCommRing` `NonUnitalNonAssocRing` `toNonUnitalNonAssocRing`	—	—

NonUnitalNonAssocCommSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	—	`toNonUnitalNonAssocSemiring_injective` `NonUnitalNonAssocSemiring.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocSemiring_injective` 📖	mathematical	—	`NonUnitalNonAssocCommSemiring` `NonUnitalNonAssocSemiring` `toNonUnitalNonAssocSemiring`	—	—

NonUnitalNonAssocRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	—	`AddCommGroup.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocSemiring_injective` 📖	mathematical	—	`NonUnitalNonAssocRing` `NonUnitalNonAssocSemiring` `toNonUnitalNonAssocSemiring`	—	`ext`

NonUnitalNonAssocSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `toDistrib` `Distrib.toMul`	—	—	`AddCommMonoid.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `toDistrib` `Distrib.toMul`	—	`ext`
`toDistrib_injective` 📖	mathematical	—	`NonUnitalNonAssocSemiring` `Distrib` `toDistrib`	—	`ext`

NonUnitalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	—	`NonUnitalNonAssocRing.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocring_injective` 📖	mathematical	—	`NonUnitalRing` `NonUnitalNonAssocRing` `toNonUnitalNonAssocRing`	—	`ext`
`toNonUnitalSemiring_injective` 📖	mathematical	—	`NonUnitalRing` `NonUnitalSemiring` `toNonUnitalSemiring`	—	`ext`

NonUnitalSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	—	`toNonUnitalNonAssocSemiring_injective` `NonUnitalNonAssocSemiring.ext`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `Distrib.toMul`	—	`ext`
`toNonUnitalNonAssocSemiring_injective` 📖	mathematical	—	`NonUnitalSemiring` `NonUnitalNonAssocSemiring` `toNonUnitalNonAssocSemiring`	—	—

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing` `Distrib.toMul`	—	—	`Semiring.ext` `NonAssocRing.ext` `AddGroup.ext` `sub_eq_add_neg` `zsmul_zero'` `zsmul_succ'` `zsmul_neg'` `neg_add_cancel` `intCast_ofNat` `intCast_negSucc`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `toNonAssocRing` `Distrib.toMul`	—	`ext`
`toNonAssocRing_injective` 📖	mathematical	—	`Ring` `NonAssocRing` `toNonAssocRing`	—	`ext`
`toNonUnitalRing_injective` 📖	mathematical	—	`Ring` `NonUnitalRing` `toNonUnitalRing`	—	`ext`
`toSemiring_injective` 📖	mathematical	—	`Ring` `Semiring` `toSemiring`	—	`ext`

Semiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring` `Distrib.toMul`	—	—	`NonUnitalSemiring.ext` `NonAssocSemiring.ext` `Monoid.ext` `one_mul` `mul_one` `natCast_zero` `natCast_succ` `NonUnitalSemiring.mul_assoc` `npow_zero` `npow_succ`
`ext_iff` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toNonAssocSemiring` `Distrib.toMul`	—	`ext`
`toNonAssocSemiring_injective` 📖	mathematical	—	`Semiring` `NonAssocSemiring` `toNonAssocSemiring`	—	`ext`
`toNonUnitalSemiring_injective` 📖	mathematical	—	`Semiring` `NonUnitalSemiring` `toNonUnitalSemiring`	—	`ext`

---

← Back to Index