Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 07:46 3045014d

View on Github →

feat(algebra/order/ring): turn mul_self_pos into an iff (#11216)

Estimated changes

Modified archive/imo/imo1998_q2.lean

Modified src/algebra/order/ring.lean

modified theorem mul_self_pos

Modified src/analysis/inner_product_space/conformal_linear_map.lean

Modified src/linear_algebra/quadratic_form/basic.lean