Theorem OrderIso.mulLeft₀_symm

Modification history

2024-11-20 10:54
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean
chore: deprecate `LinearOrderedCommGroupWithZero` lemmas (#19197) …
Added OrderIso.mulLeft₀_symmView on Github →