Theorem round_neg_two_inv

Modification history

2026-09-22 11:41
Mathlib/Algebra/Order/Round.lean
chore: use simp instead of norm_num where simp suffices (#43035) …
Modified round_neg_two_invView on Github →
2025-12-31 20:48
Mathlib/Algebra/Order/Round.lean
chore(Algebra/Order/Floor): review API about `round` (#33421)
Modified round_neg_two_invView on Github →
2025-01-19 23:29
Mathlib/Algebra/Order/Floor.lean
chore(Algebra/Order/Floor): Split off `round` section (#20831) …
Modified round_neg_two_invView on Github →
2023-01-10 17:53
Mathlib/Algebra/Order/Floor.lean
feat: port `Algebra.Order.Floor` (#1304) …
Added round_neg_two_invView on Github →