Commit 2025-07-11 15:12 ab359575

View on Github →

chore: remove space after ⅟ (#26997) This will change how the docs and infoview render, and the rules for the upcoming whitespace linter. Zulip thread: [#mathlib4 > Space after `⅟ ` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Space.20after.20.60.E2.85.9F.20.60/near/528309060)

Estimated changes

modified theorem smul_invOf_smul
modified theorem commute_invOf
modified theorem invOf_pow
modified theorem invOf_units
modified theorem invOf_eq_group_inv
modified theorem invOf_eq_left_inv
modified theorem invOf_eq_right_inv
modified theorem invOf_inj
modified theorem invOf_invOf
modified theorem invOf_mul_cancel_left'
modified theorem invOf_mul_cancel_left
modified theorem invOf_mul_cancel_right'
modified theorem invOf_mul_cancel_right
modified theorem invOf_mul_self'
modified theorem invOf_mul_self
modified theorem invOf_one'
modified theorem invOf_one
modified theorem mul_invOf_cancel_left'
modified theorem mul_invOf_cancel_left
modified theorem mul_invOf_cancel_right'
modified theorem mul_invOf_cancel_right
modified theorem mul_invOf_self'
modified theorem mul_invOf_self
modified theorem Ring.inverse_invertible
modified theorem invOf_eq_inv
modified theorem invOf_le_one
modified theorem invOf_lt_zero
modified theorem invOf_nonneg
modified theorem invOf_nonpos
modified theorem invOf_pos
modified theorem LaurentPolynomial.invOf_T
modified theorem one_sub_invOf_two
modified theorem NormedSpace.invOf_exp
modified theorem left_sub_midpoint
modified theorem left_vsub_midpoint
modified theorem midpoint_eq_smul_add
modified theorem midpoint_sub_left
modified theorem midpoint_sub_right
modified theorem midpoint_vsub_left
modified theorem midpoint_vsub_right
modified theorem right_sub_midpoint
modified theorem right_vsub_midpoint
modified theorem Matrix.det_invOf
modified theorem Matrix.invOf_eq
modified theorem Matrix.invOf_eq_nonsing_inv
modified theorem Matrix.inv_smul
modified theorem IsAlgebraic.invOf
modified theorem Derivation.leibniz_invOf