Theorem ciSup_mul_ciSup_le

Modification history

2024-10-24 21:25

Mathlib/Order/ConditionallyCompleteLattice/Group.lean

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

Modified ciSup_mul_ciSup_le View on Github →

2023-05-14 07:05

Mathlib/Order/ConditionallyCompleteLattice/Group.lean

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

Added ciSup_mul_ciSup_le View on Github →