chore(LpSpace): cleanup Fintype/Finite (#11428)

Also rename `*lpBcf` to `*lpBCF` and drop 2 duplicate instances.
leanprover-community · Mar 21, 2024 · 0f2c3bc · 0f2c3bc
1 parent 8a8d388
commit 0f2c3bc
Show file tree

Hide file tree

Showing 4 changed files with 109 additions and 84 deletions.
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -103,8 +103,8 @@ theorem PiLp.inner_apply {ι : Type*} [Fintype ι] {f : ι → Type*} [∀ i, No
 
 /-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
 space use `EuclideanSpace 𝕜 (Fin n)`. -/
-@[reducible, nolint unusedArguments]
-def EuclideanSpace (𝕜 : Type*) [IsROrC 𝕜] (n : Type*) [Fintype n] : Type _ :=
+@[reducible]
+def EuclideanSpace (𝕜 : Type*) (n : Type*) : Type _ :=
   PiLp 2 fun _ : n => 𝕜
 #align euclidean_space EuclideanSpace
 
@@ -151,20 +151,13 @@ theorem EuclideanSpace.sphere_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0
   simp_rw [mem_setOf, mem_sphere_zero_iff_norm, norm_eq, norm_eq_abs, sq_abs,
     Real.sqrt_eq_iff_sq_eq this hr, eq_comm]
 
-variable [Fintype ι]
-
 section
 
--- Porting note: no longer supported
--- attribute [local reducible] PiLp
+#align euclidean_space.finite_dimensional WithLp.instModuleFinite
 
-instance EuclideanSpace.instFiniteDimensional : FiniteDimensional 𝕜 (EuclideanSpace 𝕜 ι) := by
-  infer_instance
-#align euclidean_space.finite_dimensional EuclideanSpace.instFiniteDimensional
+variable [Fintype ι]
 
-instance EuclideanSpace.instInnerProductSpace : InnerProductSpace 𝕜 (EuclideanSpace 𝕜 ι) := by
-  infer_instance
-#align euclidean_space.inner_product_space EuclideanSpace.instInnerProductSpace
+#align euclidean_space.inner_product_space PiLp.innerProductSpace
 
 @[simp]
 theorem finrank_euclideanSpace :
@@ -253,90 +246,100 @@ def EuclideanSpace.proj (i : ι) : EuclideanSpace 𝕜 ι →L[𝕜] 𝕜 :=
 #align euclidean_space.proj_coe EuclideanSpace.proj_coe
 #align euclidean_space.proj_apply EuclideanSpace.proj_apply
 
+section DecEq
+
+variable [DecidableEq ι]
+
 -- TODO : This should be generalized to `PiLp`.
 /-- The vector given in euclidean space by being `1 : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at
 all other coordinates. -/
-def EuclideanSpace.single [DecidableEq ι] (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι :=
+def EuclideanSpace.single (i : ι) (a : 𝕜) : EuclideanSpace 𝕜 ι :=
   (WithLp.equiv _ _).symm (Pi.single i a)
 #align euclidean_space.single EuclideanSpace.single
 
 @[simp]
-theorem WithLp.equiv_single [DecidableEq ι] (i : ι) (a : 𝕜) :
+theorem WithLp.equiv_single (i : ι) (a : 𝕜) :
     WithLp.equiv _ _ (EuclideanSpace.single i a) = Pi.single i a :=
   rfl
 #align pi_Lp.equiv_single WithLp.equiv_single
 
 @[simp]
-theorem WithLp.equiv_symm_single [DecidableEq ι] (i : ι) (a : 𝕜) :
+theorem WithLp.equiv_symm_single (i : ι) (a : 𝕜) :
     (WithLp.equiv _ _).symm (Pi.single i a) = EuclideanSpace.single i a :=
   rfl
 #align pi_Lp.equiv_symm_single WithLp.equiv_symm_single
 
 @[simp]
-theorem EuclideanSpace.single_apply [DecidableEq ι] (i : ι) (a : 𝕜) (j : ι) :
+theorem EuclideanSpace.single_apply (i : ι) (a : 𝕜) (j : ι) :
     (EuclideanSpace.single i a) j = ite (j = i) a 0 := by
   rw [EuclideanSpace.single, WithLp.equiv_symm_pi_apply, ← Pi.single_apply i a j]
 #align euclidean_space.single_apply EuclideanSpace.single_apply
 
-theorem EuclideanSpace.inner_single_left [DecidableEq ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
+variable [Fintype ι]
+
+theorem EuclideanSpace.inner_single_left (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
     ⟪EuclideanSpace.single i (a : 𝕜), v⟫ = conj a * v i := by simp [apply_ite conj]
 #align euclidean_space.inner_single_left EuclideanSpace.inner_single_left
 
-theorem EuclideanSpace.inner_single_right [DecidableEq ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
+theorem EuclideanSpace.inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
     ⟪v, EuclideanSpace.single i (a : 𝕜)⟫ = a * conj (v i) := by simp [apply_ite conj, mul_comm]
 #align euclidean_space.inner_single_right EuclideanSpace.inner_single_right
 
 @[simp]
-theorem EuclideanSpace.norm_single [DecidableEq ι] (i : ι) (a : 𝕜) :
+theorem EuclideanSpace.norm_single (i : ι) (a : 𝕜) :
     ‖EuclideanSpace.single i (a : 𝕜)‖ = ‖a‖ :=
   PiLp.norm_equiv_symm_single 2 (fun _ => 𝕜) i a
 #align euclidean_space.norm_single EuclideanSpace.norm_single
 
 @[simp]
-theorem EuclideanSpace.nnnorm_single [DecidableEq ι] (i : ι) (a : 𝕜) :
+theorem EuclideanSpace.nnnorm_single (i : ι) (a : 𝕜) :
     ‖EuclideanSpace.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
   PiLp.nnnorm_equiv_symm_single 2 (fun _ => 𝕜) i a
 #align euclidean_space.nnnorm_single EuclideanSpace.nnnorm_single
 
 @[simp]
-theorem EuclideanSpace.dist_single_same [DecidableEq ι] (i : ι) (a b : 𝕜) :
+theorem EuclideanSpace.dist_single_same (i : ι) (a b : 𝕜) :
     dist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = dist a b :=
   PiLp.dist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
 #align euclidean_space.dist_single_same EuclideanSpace.dist_single_same
 
 @[simp]
-theorem EuclideanSpace.nndist_single_same [DecidableEq ι] (i : ι) (a b : 𝕜) :
+theorem EuclideanSpace.nndist_single_same (i : ι) (a b : 𝕜) :
     nndist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = nndist a b :=
   PiLp.nndist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
 #align euclidean_space.nndist_single_same EuclideanSpace.nndist_single_same
 
 @[simp]
-theorem EuclideanSpace.edist_single_same [DecidableEq ι] (i : ι) (a b : 𝕜) :
+theorem EuclideanSpace.edist_single_same (i : ι) (a b : 𝕜) :
     edist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = edist a b :=
   PiLp.edist_equiv_symm_single_same 2 (fun _ => 𝕜) i a b
 #align euclidean_space.edist_single_same EuclideanSpace.edist_single_same
 
 /-- `EuclideanSpace.single` forms an orthonormal family. -/
-theorem EuclideanSpace.orthonormal_single [DecidableEq ι] :
+theorem EuclideanSpace.orthonormal_single :
     Orthonormal 𝕜 fun i : ι => EuclideanSpace.single i (1 : 𝕜) := by
   simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
     EuclideanSpace.single_apply]
   intros
   trivial
 #align euclidean_space.orthonormal_single EuclideanSpace.orthonormal_single
 
-theorem EuclideanSpace.piLpCongrLeft_single [DecidableEq ι] {ι' : Type*} [Fintype ι']
-    [DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜) :
+theorem EuclideanSpace.piLpCongrLeft_single
+    {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜) :
     LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e (EuclideanSpace.single i' v) =
       EuclideanSpace.single (e i') v :=
   LinearIsometryEquiv.piLpCongrLeft_single e i' _
 #align euclidean_space.pi_Lp_congr_left_single EuclideanSpace.piLpCongrLeft_single
 
+end DecEq
+
 variable (ι 𝕜 E)
+variable [Fintype ι]
 
 /-- An orthonormal basis on E is an identification of `E` with its dimensional-matching
 `EuclideanSpace 𝕜 ι`. -/
 structure OrthonormalBasis where ofRepr ::
+  /-- Linear isometry between `E` and `EuclideanSpace 𝕜 ι` representing the orthonormal basis. -/
   repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
 #align orthonormal_basis OrthonormalBasis
 #align orthonormal_basis.of_repr OrthonormalBasis.ofRepr

diff --git a/Mathlib/Analysis/NormedSpace/LpEquiv.lean b/Mathlib/Analysis/NormedSpace/LpEquiv.lean
@@ -46,22 +46,24 @@ set_option linter.uppercaseLean3 false
 
 variable {α : Type*} {E : α → Type*} [∀ i, NormedAddCommGroup (E i)] {p : ℝ≥0∞}
 
+section Finite
+
+variable [Finite α]
+
 /-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`. -/
-theorem Memℓp.all [Finite α] (f : ∀ i, E i) : Memℓp f p := by
+theorem Memℓp.all (f : ∀ i, E i) : Memℓp f p := by
   rcases p.trichotomy with (rfl | rfl | _h)
   · exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite
-  · exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α => ‖f i‖).toFinite)
+  · exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)
   · cases nonempty_fintype α; exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
 #align mem_ℓp.all Memℓp.all
 
-variable [Fintype α]
-
-/-- The canonical `Equiv` between `lp E p ≃ PiLp p E` when `E : α → Type u` with `[Fintype α]`. -/
+/-- The canonical `Equiv` between `lp E p ≃ PiLp p E` when `E : α → Type u` with `[Finite α]`. -/
 def Equiv.lpPiLp : lp E p ≃ PiLp p E where
   toFun f := ⇑f
   invFun f := ⟨f, Memℓp.all f⟩
-  left_inv _f := lp.ext <| funext fun _x => rfl
-  right_inv _f := funext fun _x => rfl
+  left_inv _f := rfl
+  right_inv _f := rfl
 #align equiv.lp_pi_Lp Equiv.lpPiLp
 
 theorem coe_equiv_lpPiLp (f : lp E p) : Equiv.lpPiLp f = ⇑f :=
@@ -72,17 +74,10 @@ theorem coe_equiv_lpPiLp_symm (f : PiLp p E) : (Equiv.lpPiLp.symm f : ∀ i, E i
   rfl
 #align coe_equiv_lp_pi_Lp_symm coe_equiv_lpPiLp_symm
 
-theorem equiv_lpPiLp_norm (f : lp E p) : ‖Equiv.lpPiLp f‖ = ‖f‖ := by
-  rcases p.trichotomy with (rfl | rfl | h)
-  · simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
-  · rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]; rfl
-  · rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]; rfl
-#align equiv_lp_pi_Lp_norm equiv_lpPiLp_norm
-
 /-- The canonical `AddEquiv` between `lp E p` and `PiLp p E` when `E : α → Type u` with
 `[Fintype α]`. -/
 def AddEquiv.lpPiLp : lp E p ≃+ PiLp p E :=
-  { Equiv.lpPiLp with map_add' := fun _f _g => rfl }
+  { Equiv.lpPiLp with map_add' := fun _f _g ↦ rfl }
 #align add_equiv.lp_pi_Lp AddEquiv.lpPiLp
 
 theorem coe_addEquiv_lpPiLp  (f : lp E p) : AddEquiv.lpPiLp f = ⇑f :=
@@ -94,9 +89,18 @@ theorem coe_addEquiv_lpPiLp_symm (f : PiLp p E) :
   rfl
 #align coe_add_equiv_lp_pi_Lp_symm coe_addEquiv_lpPiLp_symm
 
+end Finite
+
+theorem equiv_lpPiLp_norm [Fintype α] (f : lp E p) : ‖Equiv.lpPiLp f‖ = ‖f‖ := by
+  rcases p.trichotomy with (rfl | rfl | h)
+  · simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
+  · rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]; rfl
+  · rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]; rfl
+#align equiv_lp_pi_Lp_norm equiv_lpPiLp_norm
+
 section Equivₗᵢ
 
-variable (𝕜 : Type*) [NontriviallyNormedField 𝕜] [∀ i, NormedSpace 𝕜 (E i)]
+variable [Fintype α] (𝕜 : Type*) [NontriviallyNormedField 𝕜] [∀ i, NormedSpace 𝕜 (E i)]
 variable (E)
 /- porting note: Lean is unable to work with `lpPiLpₗᵢ` if `E` is implicit without
 annotating with `(E := E)` everywhere, so we just make it explicit. This file has no
@@ -106,7 +110,7 @@ dependencies. -/
 with `[Fintype α]` and `[Fact (1 ≤ p)]`. -/
 noncomputable def lpPiLpₗᵢ [Fact (1 ≤ p)] : lp E p ≃ₗᵢ[𝕜] PiLp p E :=
   { AddEquiv.lpPiLp with
-    map_smul' := fun _k _f => rfl
+    map_smul' := fun _k _f ↦ rfl
     norm_map' := equiv_lpPiLp_norm }
 #align lp_pi_Lpₗᵢ lpPiLpₗᵢₓ
 -- Porting note: `#align`ed with an `ₓ` because `E` is now explicit, see above
@@ -126,7 +130,7 @@ end Equivₗᵢ
 
 end LpPiLp
 
-section LpBcf
+section LpBCF
 
 open scoped BoundedContinuousFunction
 
@@ -140,86 +144,93 @@ variable [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NonUnitalNormedRing R]
 section NormedAddCommGroup
 
 /-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as an `AddEquiv`. -/
-noncomputable def AddEquiv.lpBcf : lp (fun _ : α => E) ∞ ≃+ (α →ᵇ E) where
+noncomputable def AddEquiv.lpBCF : lp (fun _ : α ↦ E) ∞ ≃+ (α →ᵇ E) where
   toFun f := ofNormedAddCommGroupDiscrete f ‖f‖ <| le_ciSup (memℓp_infty_iff.mp f.prop)
   invFun f := ⟨⇑f, f.bddAbove_range_norm_comp⟩
   left_inv _f := lp.ext rfl
-  right_inv _f := BoundedContinuousFunction.ext fun _x => rfl
-  map_add' _f _g := BoundedContinuousFunction.ext fun _x => rfl
+  right_inv _f := rfl
+  map_add' _f _g := rfl
+#align add_equiv.lp_bcf AddEquiv.lpBCF
 
-#align add_equiv.lp_bcf AddEquiv.lpBcf
+@[deprecated] alias AddEquiv.lpBcf := AddEquiv.lpBCF -- 2024-03-16
 
-theorem coe_addEquiv_lpBcf (f : lp (fun _ : α => E) ∞) : (AddEquiv.lpBcf f : α → E) = f :=
+theorem coe_addEquiv_lpBCF (f : lp (fun _ : α ↦ E) ∞) : (AddEquiv.lpBCF f : α → E) = f :=
   rfl
-#align coe_add_equiv_lp_bcf coe_addEquiv_lpBcf
+#align coe_add_equiv_lp_bcf coe_addEquiv_lpBCF
 
-theorem coe_addEquiv_lpBcf_symm (f : α →ᵇ E) : (AddEquiv.lpBcf.symm f : α → E) = f :=
+theorem coe_addEquiv_lpBCF_symm (f : α →ᵇ E) : (AddEquiv.lpBCF.symm f : α → E) = f :=
   rfl
-#align coe_add_equiv_lp_bcf_symm coe_addEquiv_lpBcf_symm
+#align coe_add_equiv_lp_bcf_symm coe_addEquiv_lpBCF_symm
 
 variable (E)
 /- porting note: Lean is unable to work with `lpPiLpₗᵢ` if `E` is implicit without
 annotating with `(E := E)` everywhere, so we just make it explicit. This file has no
 dependencies. -/
 
 /-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as a `LinearIsometryEquiv`. -/
-noncomputable def lpBcfₗᵢ : lp (fun _ : α => E) ∞ ≃ₗᵢ[𝕜] α →ᵇ E :=
-  { AddEquiv.lpBcf with
-    map_smul' := fun k f => rfl
-    norm_map' := fun f => by simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]; rfl }
-#align lp_bcfₗᵢ lpBcfₗᵢₓ
+noncomputable def lpBCFₗᵢ : lp (fun _ : α ↦ E) ∞ ≃ₗᵢ[𝕜] α →ᵇ E :=
+  { AddEquiv.lpBCF with
+    map_smul' := fun k f ↦ rfl
+    norm_map' := fun f ↦ by simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]; rfl }
+#align lp_bcfₗᵢ lpBCFₗᵢₓ
 -- Porting note: `#align`ed with an `ₓ` because `E` is now explicit, see above
 
+@[deprecated] alias lpBcfₗᵢ := lpBCFₗᵢ -- 2024-03-16
+
 variable {𝕜 E}
 
-theorem coe_lpBcfₗᵢ (f : lp (fun _ : α => E) ∞) : (lpBcfₗᵢ E 𝕜 f : α → E) = f :=
+theorem coe_lpBCFₗᵢ (f : lp (fun _ : α ↦ E) ∞) : (lpBCFₗᵢ E 𝕜 f : α → E) = f :=
   rfl
-#align coe_lp_bcfₗᵢ coe_lpBcfₗᵢ
+#align coe_lp_bcfₗᵢ coe_lpBCFₗᵢ
 
-theorem coe_lpBcfₗᵢ_symm (f : α →ᵇ E) : ((lpBcfₗᵢ E 𝕜).symm f : α → E) = f :=
+theorem coe_lpBCFₗᵢ_symm (f : α →ᵇ E) : ((lpBCFₗᵢ E 𝕜).symm f : α → E) = f :=
   rfl
-#align coe_lp_bcfₗᵢ_symm coe_lpBcfₗᵢ_symm
+#align coe_lp_bcfₗᵢ_symm coe_lpBCFₗᵢ_symm
 
 end NormedAddCommGroup
 
 section RingAlgebra
 
 /-- The canonical map between `lp (fun _ : α ↦ R) ∞` and `α →ᵇ R` as a `RingEquiv`. -/
-noncomputable def RingEquiv.lpBcf : lp (fun _ : α => R) ∞ ≃+* (α →ᵇ R) :=
-  { @AddEquiv.lpBcf _ R _ _ _ with
-    map_mul' := fun _f _g => BoundedContinuousFunction.ext fun _x => rfl }
-#align ring_equiv.lp_bcf RingEquiv.lpBcf
+noncomputable def RingEquiv.lpBCF : lp (fun _ : α ↦ R) ∞ ≃+* (α →ᵇ R) :=
+  { @AddEquiv.lpBCF _ R _ _ _ with
+    map_mul' := fun _f _g => rfl }
+#align ring_equiv.lp_bcf RingEquiv.lpBCF
+
+@[deprecated] alias RingEquiv.lpBcf := RingEquiv.lpBCF -- 2024-03-16
 
 variable {R}
 
-theorem coe_ringEquiv_lpBcf (f : lp (fun _ : α => R) ∞) : (RingEquiv.lpBcf R f : α → R) = f :=
+theorem coe_ringEquiv_lpBCF (f : lp (fun _ : α ↦ R) ∞) : (RingEquiv.lpBCF R f : α → R) = f :=
   rfl
-#align coe_ring_equiv_lp_bcf coe_ringEquiv_lpBcf
+#align coe_ring_equiv_lp_bcf coe_ringEquiv_lpBCF
 
-theorem coe_ringEquiv_lpBcf_symm (f : α →ᵇ R) : ((RingEquiv.lpBcf R).symm f : α → R) = f :=
+theorem coe_ringEquiv_lpBCF_symm (f : α →ᵇ R) : ((RingEquiv.lpBCF R).symm f : α → R) = f :=
   rfl
-#align coe_ring_equiv_lp_bcf_symm coe_ringEquiv_lpBcf_symm
+#align coe_ring_equiv_lp_bcf_symm coe_ringEquiv_lpBCF_symm
 
 variable (α)
 
 -- even `α` needs to be explicit here for elaboration
 -- the `NormOneClass A` shouldn't really be necessary, but currently it is for
 -- `one_memℓp_infty` to get the `Ring` instance on `lp`.
 /-- The canonical map between `lp (fun _ : α ↦ A) ∞` and `α →ᵇ A` as an `AlgEquiv`. -/
-noncomputable def AlgEquiv.lpBcf : lp (fun _ : α => A) ∞ ≃ₐ[𝕜] α →ᵇ A :=
-  { RingEquiv.lpBcf A with commutes' := fun _k => rfl }
-#align alg_equiv.lp_bcf AlgEquiv.lpBcf
+noncomputable def AlgEquiv.lpBCF : lp (fun _ : α ↦ A) ∞ ≃ₐ[𝕜] α →ᵇ A :=
+  { RingEquiv.lpBCF A with commutes' := fun _k ↦ rfl }
+#align alg_equiv.lp_bcf AlgEquiv.lpBCF
+
+@[deprecated] alias AlgEquiv.lpBcf := AlgEquiv.lpBCF -- 2024-03-16
 
 variable {α A 𝕜}
 
-theorem coe_algEquiv_lpBcf (f : lp (fun _ : α => A) ∞) : (AlgEquiv.lpBcf α A 𝕜 f : α → A) = f :=
+theorem coe_algEquiv_lpBCF (f : lp (fun _ : α ↦ A) ∞) : (AlgEquiv.lpBCF α A 𝕜 f : α → A) = f :=
   rfl
-#align coe_alg_equiv_lp_bcf coe_algEquiv_lpBcf
+#align coe_alg_equiv_lp_bcf coe_algEquiv_lpBCF
 
-theorem coe_algEquiv_lpBcf_symm (f : α →ᵇ A) : ((AlgEquiv.lpBcf α A 𝕜).symm f : α → A) = f :=
+theorem coe_algEquiv_lpBCF_symm (f : α →ᵇ A) : ((AlgEquiv.lpBCF α A 𝕜).symm f : α → A) = f :=
   rfl
-#align coe_alg_equiv_lp_bcf_symm coe_algEquiv_lpBcf_symm
+#align coe_alg_equiv_lp_bcf_symm coe_algEquiv_lpBCF_symm
 
 end RingAlgebra
 
-end LpBcf
+end LpBCF