From 780362f4d0dcc403e2ac70850214575fbeaaacc0 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 9 Apr 2023 07:30:15 +0000 Subject: [PATCH] fix: `inv_of` -> `invOf` (#3336) --- Mathlib/Algebra/Module/Basic.lean | 4 ++-- Mathlib/Algebra/Star/Module.lean | 2 +- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean index 19f3832dfcf3ac..58de3619fc66d2 100644 --- 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 index cf7307e8bb8830..2437a488f28bbe 100644 --- 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 index aec49025759a41..78875ebeba83a4 100644 --- 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