fix: inv_of -> invOf (#3336)

leanprover-community · Apr 9, 2023 · 780362f · 780362f
1 parent 229e24e
commit 780362f
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -112,10 +112,10 @@ set_option linter.deprecated false in
 #align two_smul' two_smul'
 
 @[simp]
-theorem inv_of_two_smul_add_inv_of_two_smul [Invertible (2 : R)] (x : M) :
+theorem invOf_two_smul_add_invOf_two_smul [Invertible (2 : R)] (x : M) :
     (⅟ 2 : R) • x + (⅟ 2 : R) • x = x :=
   Convex.combo_self invOf_two_add_invOf_two _
-#align inv_of_two_smul_add_inv_of_two_smul inv_of_two_smul_add_inv_of_two_smul
+#align inv_of_two_smul_add_inv_of_two_smul invOf_two_smul_add_invOf_two_smul
 
 /-- Pullback a `Module` structure along an injective additive monoid homomorphism.
 See note [reducible non-instances]. -/

diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
@@ -144,7 +144,7 @@ def skewAdjointPart : A →ₗ[R] skewAdjoint A
 theorem StarModule.selfAdjointPart_add_skewAdjointPart (x : A) :
     (selfAdjointPart R x : A) + skewAdjointPart R x = x := by
   simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe,
-    add_add_sub_cancel, inv_of_two_smul_add_inv_of_two_smul]
+    add_add_sub_cancel, invOf_two_smul_add_invOf_two_smul]
 #align star_module.self_adjoint_part_add_skew_adjoint_part StarModule.selfAdjointPart_add_skewAdjointPart
 
 variable (A)

diff --git a/Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean b/Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
@@ -127,7 +127,7 @@ theorem right_vsub_midpoint (p₁ p₂ : P) : p₂ -ᵥ midpoint R p₁ p₂ = (
 theorem midpoint_vsub (p₁ p₂ p : P) :
     midpoint R p₁ p₂ -ᵥ p = (⅟ 2 : R) • (p₁ -ᵥ p) + (⅟ 2 : R) • (p₂ -ᵥ p) := by
   rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
-    neg_vsub_eq_vsub_rev, add_assoc, inv_of_two_smul_add_inv_of_two_smul, ← vadd_vsub_assoc,
+    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
     midpoint_comm, midpoint, lineMap_apply]
 #align midpoint_vsub midpoint_vsub