Documentation Verification Report

RatAlgebra

📁 Source: Mathlib/RingTheory/DividedPowers/RatAlgebra.lean

Statistics

Metric	Count
Definitions `dividedPowers`, `dividedPowers`, `dividedPowers`, `dpow`, `dividedPowers`, `dividedPowers`, `dpow`	7
Theorems `dpow_of_prime_le`, `dpow_of_prime_le`, `dpow_add`, `dpow_add_of_lt`, `dpow_apply`, `dpow_comp`, `dpow_comp_of_mul_lt`, `dpow_eq_of_mem`, `dpow_eq_of_not_mem`, `dpow_mem`, `dpow_mul`, `dpow_mul_of_add_lt`, `dpow_null`, `dpow_one`, `dpow_zero`, `mul_dpow`, `dpow_of_two_le`, `dividedPowers_unique`, `dpow_apply`, `dpow_eq_inv_fact_smul`, `dpow_eq_of_mem`	21
Total	28

DividedPowers.CharP

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	1 math math: `dpow_of_prime_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_of_prime_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`DividedPowers.dpow` `dividedPowers` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IsScalarTower.right` `Ideal.pow_eq_zero_of_mem` `MulZeroClass.mul_zero`

DividedPowers.IsNilpotent

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	1 math math: `dpow_of_prime_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_of_prime_le` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Ideal` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`DividedPowers.dpow` `dividedPowers`	—	`IsScalarTower.right` `Ideal.pow_eq_zero_of_mem` `MulZeroClass.mul_zero`

DividedPowers.OfInvertibleFactorial

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	1 math math: `dpow_apply`
`dpow` 📖	CompOp	13 math math: `dpow_mem`, `dpow_comp`, `dpow_add`, `dpow_zero`, `dpow_null`, `dpow_one`, `mul_dpow`, `dpow_eq_of_not_mem`, `dpow_comp_of_mul_lt`, `dpow_eq_of_mem`, `dpow_add_of_lt`, `dpow_mul_of_add_lt`, `dpow_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_add` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike`	`dpow` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Distrib.toMul`	—	`IsScalarTower.right` `dpow_add_of_lt` `Ideal.pow_le_pow_right` `dpow_eq_of_mem` `Ideal.add_mem` `Finset.sum_congr` `Ideal.mem_bot` `Ideal.zero_eq_bot` `Set.mem_of_subset_of_mem` `Ideal.pow_mem_pow` `MulZeroClass.mul_zero` `Finset.sum_eq_zero` `mul_assoc` `mul_comm` `mul_eq_zero_of_right` `Finset.HasAntidiagonal.mem_antidiagonal` `add_comm` `pow_add` `Ideal.mul_mem_mul`
`dpow_add_of_lt` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`dpow` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Distrib.toMul`	—	`dpow_eq_of_mem` `Ideal.add_mem` `Finset.sum_congr` `Ring.inverse_mul_eq_iff_eq_mul` `IsUnit.natCast_factorial_of_lt` `Finset.mul_sum` `Commute.add_pow'` `Commute.all` `Mathlib.Tactic.Ring.nsmul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.smul_eq_cast` `Mathlib.Tactic.Ring.natCast_add` `Mathlib.Tactic.Ring.natCast_mul` `Mathlib.Tactic.Ring.natCast_nat` `Mathlib.Tactic.Ring.natCast_zero` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `mul_assoc` `Nat.castChoose_eq`
`dpow_apply` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`DividedPowers.dpow` `dividedPowers` `SetLike.instMembership` `Submodule.setLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ring.inverse` `Monoid.toNatPow` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsScalarTower.right`
`dpow_comp` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike`	`dpow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Nat.uniformBell`	—	`IsScalarTower.right` `dpow_comp_of_mul_lt` `Ideal.pow_eq_zero_of_mem` `dpow_eq_of_mem` `dpow_mem` `mul_pow` `pow_mul` `mul_assoc` `mul_comm` `MulZeroClass.mul_zero`
`dpow_comp_of_mul_lt` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`dpow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Nat.uniformBell`	—	`lt_of_le_of_lt` `dpow_eq_of_mem` `dpow_mem` `pow_zero` `mul_one` `Nat.uniformBell_zero_left` `Nat.cast_one` `MulZeroClass.zero_mul` `one_mul` `mul_pow` `pow_mul` `mul_comm` `mul_assoc` `Ring.eq_mul_inverse_iff_mul_eq` `IsUnit.natCast_factorial_of_lt` `Ring.inverse_mul_eq_iff_eq_mul` `Ring.inverse_pow_mul_eq_iff_eq_mul` `Nat.uniformBell_mul_eq` `Nat.cast_mul` `Nat.cast_pow` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero`
`dpow_eq_of_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ring.inverse` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.factorial` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	—
`dpow_eq_of_not_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`dpow_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow`	—	`dpow_eq_of_mem` `Ideal.mul_mem_left` `Ideal.pow_mem_of_mem`
`dpow_mul` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`dpow_eq_of_mem` `Ideal.mul_mem_left` `mul_pow` `mul_assoc` `mul_comm`
`dpow_mul_of_add_lt` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `dpow` `Nat.choose`	—	`lt_of_le_of_lt` `le_self_add` `Nat.instCanonicallyOrderedAdd` `le_add_self` `dpow_eq_of_mem` `mul_assoc` `mul_comm` `pow_add` `Ring.eq_mul_inverse_iff_mul_eq` `IsUnit.natCast_factorial_of_lt` `Ring.inverse_mul_eq_iff_eq_mul` `Nat.add_choose_mul_factorial_mul_factorial` `Nat.choose_symm_add`
`dpow_null` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`dpow_one` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow`	—	`dpow_eq_of_mem` `Nat.cast_one` `Ring.inverse_one` `pow_one` `one_mul`
`dpow_zero` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.cast_one` `Ring.inverse_one` `pow_zero` `mul_one`
`mul_dpow` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.factorial` `Ideal` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `dpow` `Nat.choose`	—	`IsScalarTower.right` `dpow_mul_of_add_lt` `Ideal.pow_eq_zero_of_mem` `dpow_eq_of_mem` `mul_assoc` `mul_comm` `pow_add` `MulZeroClass.mul_zero`

DividedPowers.OfSquareZero

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	1 math math: `dpow_of_two_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_of_two_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow` `dividedPowers` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Ideal.pow_eq_zero_of_mem` `MulZeroClass.mul_zero`

DividedPowers.RatAlgebra

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	2 math math: `dividedPowers_unique`, `dpow_apply`
`dpow` 📖	CompOp	1 math math: `dpow_eq_of_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dividedPowers_unique` 📖	mathematical	—	`dividedPowers`	—	`DividedPowers.ext` `dpow_apply` `Ring.inverse_mul_eq_iff_eq_mul` `IsUnit.natCast_factorial_of_algebra` `Rat.instCharZero` `DividedPowers.factorial_mul_dpow_eq_pow`
`dpow_apply` 📖	mathematical	—	`DividedPowers.dpow` `dividedPowers` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ring.inverse` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.factorial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`dpow_eq_inv_fact_smul` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow` `Algebra.toSMul` `Rat.commSemiring` `Ring.inverse` `Semiring.toMonoidWithZero` `Rat.semiring` `Nat.factorial` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`Ring.inverse_eq_inv'` `DividedPowers.factorial_mul_dpow_eq_pow` `smul_eq_mul` `smul_assoc` `IsScalarTower.right` `one_smul` `Nat.cast_smul_eq_nsmul` `nsmul_eq_mul` `mul_one` `SemigroupAction.mul_smul` `Nat.cast_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero`
`dpow_eq_of_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`dpow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ring.inverse` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.factorial` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`dpow.eq_1` `DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem`

---

← Back to Index