Documentation Verification Report

ReduceModChar

📁 Source: Mathlib/Tactic/ReduceModChar.lean

Statistics

Metric	Count
Definitions `TypeToCharPResult`, `derive`, `instInhabitedTypeToCharPResult`, `matchAndNorm`, `normBareNumeral`, `normIntNumeral`, `normIntNumeral'`, `normNeg`, `normNegCoeffMul`, `normPow`, `reduce_mod_char!`, `typeToCharP`	12
Theorems `intCast_eq_mod`, `isInt_of_mod`, `isNat_pow`, `neg_eq_sub_one_mul`, `neg_mul_eq_sub_one_mul`	5
Total	17

Tactic.ReduceModChar

Definitions

Name	Category	Theorems
`TypeToCharPResult` 📖	CompData	—
`derive` 📖	CompOp	—
`instInhabitedTypeToCharPResult` 📖	CompOp	—
`matchAndNorm` 📖	CompOp	—
`normBareNumeral` 📖	CompOp	—
`normIntNumeral` 📖	CompOp	—
`normIntNumeral'` 📖	CompOp	—
`normNeg` 📖	CompOp	—
`normNegCoeffMul` 📖	CompOp	—
`normPow` 📖	CompOp	—
`reduce_mod_char!` 📖	CompOp	—
`typeToCharP` 📖	CompOp	—

Tactic.ReduceModChar.CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_eq_mod` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`CharP.intCast_eq_intCast_mod`
`isInt_of_mod` 📖	—	`Mathlib.Meta.NormNum.IsInt` `Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne` `Int.instRing`	—	—	`Mathlib.Meta.NormNum.IsInt.out` `CharP.intCast_eq_intCast_mod` `Mathlib.Meta.NormNum.IsNat.out`
`isNat_pow` 📖	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Mathlib.Meta.NormNum.IsNat` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instAddMonoidWithOne`	—	—	`Nat.cast_id` `Nat.cast_pow` `CharP.natCast_eq_natCast_mod`
`neg_eq_sub_one_mul` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Mathlib.Meta.NormNum.IsNat.out` `neg_one_mul` `neg_mul` `one_mul` `CharP.cast_eq_zero` `zero_sub`
`neg_mul_eq_sub_one_mul` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Mathlib.Meta.NormNum.IsNat.out` `neg_one_mul` `neg_mul` `one_mul` `CharP.cast_eq_zero` `zero_sub`

---

← Back to Index