mathlib documentation

Equations

• char.decidable_linear_order = {le := has_le.le char.has_le, lt := has_lt.lt char.has_lt, le_refl := char.decidable_linear_order._proof_1, le_trans := char.decidable_linear_order._proof_2, lt_iff_le_not_le := char.decidable_linear_order._proof_3, le_antisymm := char.decidable_linear_order._proof_4, le_total := char.decidable_linear_order._proof_5, decidable_le := char.decidable_le, decidable_eq := char.decidable_eq, decidable_lt := char.decidable_lt}