Documentation Verification Report

Lex

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

Statistics

Metric	Count
Definitions `fst`, `fstₗ`, `inl`, `inlₗ`, `inr`, `inrₗ`, `snd`, `fst`, `fstₗ`, `inl`, `inlₗ`, `inr`, `inrₗ`, `snd`	14
Theorems `fst_mono`, `inl_mono`, `inl_strictMono`, `inr_mono`, `inr_strictMono`, `snd_mono`, `fst_mono`, `inl_mono`, `inl_strictMono`, `inr_mono`, `inr_strictMono`, `snd_mono`, `addCommute_inl_inr`, `addCommute_inlₗ_inrₗ`, `fst_apply`, `fst_comp_inl`, `fst_comp_inr`, `fstₗ_apply`, `fstₗ_comp_inlₗ`, `inl_add_inr_eq_mk`, `inl_apply`, `inlₗ_add_inrₗ_eq_toLex`, `inlₗ_apply`, `inr_apply`, `inrₗ_apply`, `snd_apply`, `snd_comp_inl`, `snd_comp_inr`, `commute_inl_inr`, `commute_inlₗ_inrₗ`, `fst_apply`, `fst_comp_inl`, `fst_comp_inr`, `fstₗ_apply`, `fstₗ_comp_inlₗ`, `inl_apply`, `inl_mul_inr_eq_mk`, `inlₗ_apply`, `inlₗ_mul_inrₗ_eq_toLex`, `inr_apply`, `inrₗ_apply`, `snd_apply`, `snd_comp_inl`, `snd_comp_inr`	44
Total	58

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `fst`	—	`Prod.le_def`
`inl_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inl`	—	`le_refl`
`inl_strictMono` 📖	mathematical	—	`StrictMono` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inl`	—	`le_refl` `lt_self_iff_false`
`inr_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inr`	—	`le_refl`
`inr_strictMono` 📖	mathematical	—	`StrictMono` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inr`	—	`lt_self_iff_false` `le_refl`
`snd_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `snd`	—	`Prod.le_def`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `instFunLike` `fst`	—	—
`inl_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inl`	—	—
`inl_strictMono` 📖	mathematical	—	`StrictMono` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inl`	—	—
`inr_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inr`	—	—
`inr_strictMono` 📖	mathematical	—	`StrictMono` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inr`	—	—
`snd_mono` 📖	mathematical	—	`Monotone` `Prod.instPreorder` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `instFunLike` `snd`	—	—

OrderAddMonoidHom

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	3 math math: `fst_comp_inl`, `fst_comp_inr`, `fst_apply`
`fstₗ` 📖	CompOp	2 math math: `fstₗ_comp_inlₗ`, `fstₗ_apply`
`inl` 📖	CompOp	5 math math: `inl_apply`, `fst_comp_inl`, `addCommute_inl_inr`, `inl_add_inr_eq_mk`, `snd_comp_inl`
`inlₗ` 📖	CompOp	4 math math: `addCommute_inlₗ_inrₗ`, `fstₗ_comp_inlₗ`, `inlₗ_apply`, `inlₗ_add_inrₗ_eq_toLex`
`inr` 📖	CompOp	5 math math: `addCommute_inl_inr`, `snd_comp_inr`, `inr_apply`, `fst_comp_inr`, `inl_add_inr_eq_mk`
`inrₗ` 📖	CompOp	3 math math: `addCommute_inlₗ_inrₗ`, `inlₗ_add_inrₗ_eq_toLex`, `inrₗ_apply`
`snd` 📖	CompOp	3 math math: `snd_comp_inr`, `snd_apply`, `snd_comp_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommute_inl_inr` 📖	mathematical	—	`AddCommute` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `Prod.instAddZeroClass` `instFunLike` `inl` `inr`	—	`AddCommute.prod` `AddCommute.zero_right` `AddCommute.zero_left`
`addCommute_inlₗ_inrₗ` 📖	mathematical	—	`AddCommute` `Lex` `instAddLex` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `instAddZeroClassLex` `Prod.instAddZeroClass` `instFunLike` `inlₗ` `inrₗ`	—	`AddCommute.prod` `AddCommute.zero_right` `AddCommute.zero_left`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `fst`	—	—
`fst_comp_inl` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `Prod.instPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `fst` `inl` `id`	—	—
`fst_comp_inr` 📖	mathematical	—	`comp` `Prod.instPreorder` `PartialOrder.toPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `fst` `inr` `OrderAddMonoidHom` `instZero`	—	—
`fstₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Lex` `Prod.Lex.instPreorder` `PartialOrder.toPreorder` `instAddZeroClassLex` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `fstₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`fstₗ_comp_inlₗ` 📖	mathematical	—	`comp` `Lex` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `AddMonoid.toAddZeroClass` `instAddZeroClassLex` `Prod.instAddZeroClass` `fstₗ` `inlₗ` `id`	—	—
`inl_add_inr_eq_mk` 📖	mathematical	—	`Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `Prod.instAddZeroClass` `instFunLike` `inl` `inr`	—	`add_zero` `zero_add`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`inlₗ_add_inrₗ_eq_toLex` 📖	mathematical	—	`Lex` `instAddLex` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `instAddZeroClassLex` `Prod.instAddZeroClass` `instFunLike` `inlₗ` `inrₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`add_zero` `zero_add`
`inlₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Lex` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `AddMonoid.toAddZeroClass` `instAddZeroClassLex` `Prod.instAddZeroClass` `instFunLike` `inlₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `instFunLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`inrₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Lex` `Prod.Lex.instPreorder` `PartialOrder.toPreorder` `AddMonoid.toAddZeroClass` `instAddZeroClassLex` `Prod.instAddZeroClass` `instFunLike` `inrₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `AddZero.toZero` `AddZeroClass.toAddZero`	—	—
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `snd`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `Prod.instPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `snd` `inl` `OrderAddMonoidHom` `instZero`	—	—
`snd_comp_inr` 📖	mathematical	—	`comp` `Prod.instPreorder` `PartialOrder.toPreorder` `AddMonoid.toAddZeroClass` `Prod.instAddZeroClass` `snd` `inr` `id`	—	—

OrderMonoidHom

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	3 math math: `fst_apply`, `fst_comp_inr`, `fst_comp_inl`
`fstₗ` 📖	CompOp	2 math math: `fstₗ_apply`, `fstₗ_comp_inlₗ`
`inl` 📖	CompOp	5 math math: `inl_mul_inr_eq_mk`, `commute_inl_inr`, `snd_comp_inl`, `inl_apply`, `fst_comp_inl`
`inlₗ` 📖	CompOp	5 math math: `inlₗ_mul_inrₗ_eq_toLex`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `inlₗ_apply`, `commute_inlₗ_inrₗ`, `fstₗ_comp_inlₗ`
`inr` 📖	CompOp	5 math math: `inl_mul_inr_eq_mk`, `commute_inl_inr`, `snd_comp_inr`, `fst_comp_inr`, `inr_apply`
`inrₗ` 📖	CompOp	4 math math: `inrₗ_apply`, `inlₗ_mul_inrₗ_eq_toLex`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `commute_inlₗ_inrₗ`
`snd` 📖	CompOp	3 math math: `snd_comp_inl`, `snd_apply`, `snd_comp_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_inl_inr` 📖	mathematical	—	`Commute` `Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `OrderMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `Prod.instMulOneClass` `instFunLike` `inl` `inr`	—	`Commute.prod` `Commute.one_right` `Commute.one_left`
`commute_inlₗ_inrₗ` 📖	mathematical	—	`Commute` `Lex` `instMulLex` `Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `OrderMonoidHom` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `instMulOneClassLex` `Prod.instMulOneClass` `instFunLike` `inlₗ` `inrₗ`	—	`Commute.prod` `Commute.one_right` `Commute.one_left`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `Prod.instMulOneClass` `Monoid.toMulOneClass` `instFunLike` `fst`	—	—
`fst_comp_inl` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `Prod.instPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `fst` `inl` `id`	—	—
`fst_comp_inr` 📖	mathematical	—	`comp` `Prod.instPreorder` `PartialOrder.toPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `fst` `inr` `OrderMonoidHom` `instOne`	—	—
`fstₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Lex` `Prod.Lex.instPreorder` `PartialOrder.toPreorder` `instMulOneClassLex` `Prod.instMulOneClass` `Monoid.toMulOneClass` `instFunLike` `fstₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`fstₗ_comp_inlₗ` 📖	mathematical	—	`comp` `Lex` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `Monoid.toMulOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `fstₗ` `inlₗ` `id`	—	—
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inl` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`inl_mul_inr_eq_mk` 📖	mathematical	—	`Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `OrderMonoidHom` `PartialOrder.toPreorder` `Prod.instPreorder` `Prod.instMulOneClass` `instFunLike` `inl` `inr`	—	`mul_one` `one_mul`
`inlₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Lex` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `Monoid.toMulOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `instFunLike` `inlₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`inlₗ_mul_inrₗ_eq_toLex` 📖	mathematical	—	`Lex` `instMulLex` `Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `OrderMonoidHom` `PartialOrder.toPreorder` `Prod.Lex.instPreorder` `instMulOneClassLex` `Prod.instMulOneClass` `instFunLike` `inlₗ` `inrₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`mul_one` `one_mul`
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `instFunLike` `inr` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`inrₗ_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Lex` `Prod.Lex.instPreorder` `PartialOrder.toPreorder` `Monoid.toMulOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `instFunLike` `inrₗ` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `MulOne.toOne` `MulOneClass.toMulOne`	—	—
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidHom` `Prod.instPreorder` `PartialOrder.toPreorder` `Prod.instMulOneClass` `Monoid.toMulOneClass` `instFunLike` `snd`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `PartialOrder.toPreorder` `Prod.instPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `snd` `inl` `OrderMonoidHom` `instOne`	—	—
`snd_comp_inr` 📖	mathematical	—	`comp` `Prod.instPreorder` `PartialOrder.toPreorder` `Monoid.toMulOneClass` `Prod.instMulOneClass` `snd` `inr` `id`	—	—

---

← Back to Index