Documentation Verification Report

ToMulBot

📁 Source: Mathlib/Algebra/Order/Monoid/ToMulBot.lean

Statistics

Metric	Count
Definitions `toMulBot`	1
Theorems `toMulBot_coe`, `toMulBot_coe_ofAdd`, `toMulBot_le`, `toMulBot_lt`, `toMulBot_strictMono`, `toMulBot_symm_bot`, `toMulBot_zero`	7
Total	8

WithZero

Definitions

Name	Category	Theorems
`toMulBot` 📖	CompOp	7 math math: `toMulBot_lt`, `toMulBot_coe_ofAdd`, `toMulBot_zero`, `toMulBot_coe`, `toMulBot_le`, `toMulBot_symm_bot`, `toMulBot_strictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMulBot_coe` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Multiplicative` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `WithBot.add` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulBot` `coe` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `WithBot.some` `Multiplicative.toAdd`	—	—
`toMulBot_coe_ofAdd` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Multiplicative` `WithBot` `WithZero` `Multiplicative.mul` `WithBot.add` `MulZeroClass.toMul` `instMulZeroClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toMulBot` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `WithBot.some` `coe`	—	—
`toMulBot_le` 📖	mathematical	—	`Multiplicative` `WithBot` `instLEMultiplicative` `Preorder.toLE` `WithBot.instPreorder` `DFunLike.coe` `MulEquiv` `WithZero` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `WithBot.add` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulBot` `instPreorder` `Multiplicative.preorder`	—	—
`toMulBot_lt` 📖	mathematical	—	`Multiplicative` `WithBot` `instLTMultiplicative` `Preorder.toLT` `WithBot.instPreorder` `DFunLike.coe` `MulEquiv` `WithZero` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `WithBot.add` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulBot` `instPreorder` `Multiplicative.preorder`	—	—
`toMulBot_strictMono` 📖	mathematical	—	`StrictMono` `WithZero` `Multiplicative` `WithBot` `instPreorder` `Multiplicative.preorder` `WithBot.instPreorder` `DFunLike.coe` `MulEquiv` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `WithBot.add` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulBot`	—	—
`toMulBot_symm_bot` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Multiplicative` `WithBot` `WithZero` `Multiplicative.mul` `WithBot.add` `MulZeroClass.toMul` `instMulZeroClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `toMulBot` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Bot.bot` `WithBot.bot` `instZero`	—	—
`toMulBot_zero` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Multiplicative` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `WithBot.add` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toMulBot` `instZero` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Bot.bot` `WithBot.bot`	—	—

---

← Back to Index