Commit 2023-04-09 07:30 da1bd9ef

View on Github →

fix: inv_of -> invOf (#3336)

Estimated changes

Modified Mathlib/Algebra/Module/Basic.lean

added theorem invOf_two_smul_add_invOf_two_smul

deleted theorem inv_of_two_smul_add_inv_of_two_smul

Modified Mathlib/Algebra/Star/Module.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean