Documentation Verification Report

Rat

📁 Source: Mathlib/Algebra/Ring/Action/Rat.lean

Statistics

Metric	Count
Definitions `instDistribSMul`, `instDistribSMul`	2
Theorems `instIsScalarTowerRight`, `instIsScalarTowerRight`	2
Total	4

NNRat

Definitions

Name	Category	Theorems
`instDistribSMul` 📖	CompOp	6 math math: `Polynomial.nnqsmul_eq_C_mul`, `Complex.im_nnqsmul`, `NNReal.coe_nnqsmul`, `instIsScalarTowerRight`, `Complex.re_nnqsmul`, `Complex.ofReal_nnqsmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerRight` 📖	mathematical	—	`IsScalarTower` `NNRat` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`smul_def` `mul_assoc`

Rat

Definitions

Name	Category	Theorems
`instDistribSMul` 📖	CompOp	5 math math: `Complex.im_qsmul`, `instIsScalarTowerRight`, `Complex.re_qsmul`, `Complex.ofReal_qsmul`, `Polynomial.qsmul_eq_C_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerRight` 📖	mathematical	—	`IsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `DistribSMul.toSMulZeroClass` `instDistribSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`smul_def` `mul_assoc`

---

← Back to Index