Theorem le_ciInf_mul

Modification history

2024-10-24 21:25

Mathlib/Order/ConditionallyCompleteLattice/Group.lean

feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)

Modified le_ciInf_mul View on Github →

2023-05-14 07:05

Mathlib/Order/ConditionallyCompleteLattice/Group.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added le_ciInf_mul View on Github →