Theorem sq_le_one_iff

Modification history

2024-11-14 11:04

Mathlib/Algebra/Order/Ring/Basic.lean

chore: generalise pow monotonicity lemmas to groups with zero (#18967) …

Modified sq_le_one_iff View on Github →

2022-12-15 21:58

Mathlib/Algebra/GroupPower/Order.lean

feat: port Algebra.GroupPower.Order (#1043) …

Added sq_le_one_iff View on Github →