[Merged by Bors] - chore: classify broken dot notation porting notes

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -36,7 +36,7 @@ def kernelCone : KernelFork f :=
 def kernelIsLimit : IsLimit (kernelCone f) :=
   Fork.IsLimit.mk _
     (fun s =>
-    -- Porting note: broken dot notation on LinearMap.ker
+    -- Porting note (#11036): broken dot notation on LinearMap.ker
       LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) fun c =>
         LinearMap.mem_ker.2 <| by
           -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
@@ -58,10 +58,10 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
     (fun s =>
       f.range.liftQ (Cofork.π s) <| LinearMap.range_le_ker_iff.2 <| CokernelCofork.condition s)
     (fun s => f.range.liftQ_mkQ (Cofork.π s) _) fun s m h => by
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
     haveI : Epi (asHom (LinearMap.range f).mkQ) :=
       (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
     apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
     convert h
     -- Porting note: no longer necessary
@@ -92,22 +92,22 @@ variable {G H : ModuleCat.{v} R} (f : G ⟶ H)
 agrees with the usual module-theoretical kernel.
 -/
 noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
     kernel f ≅ ModuleCat.of R (LinearMap.ker f) :=
   limit.isoLimitCone ⟨_, kernelIsLimit f⟩
 #align Module.kernel_iso_ker ModuleCat.kernelIsoKer
 
 -- We now show this isomorphism commutes with the inclusion of the kernel into the source.
 @[simp, elementwise]
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
 theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f =
     (LinearMap.ker f).subtype :=
   limit.isoLimitCone_inv_π _ _
 #align Module.kernel_iso_ker_inv_kernel_ι ModuleCat.kernelIsoKer_inv_kernel_ι
 
 @[simp, elementwise]
 theorem kernelIsoKer_hom_ker_subtype :
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
     (kernelIsoKer f).hom ≫ (LinearMap.ker f).subtype = kernel.ι f :=
   IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) WalkingParallelPair.zero
 #align Module.kernel_iso_ker_hom_ker_subtype ModuleCat.kernelIsoKer_hom_ker_subtype
@@ -116,7 +116,7 @@ theorem kernelIsoKer_hom_ker_subtype :
 agrees with the usual module-theoretical quotient.
 -/
 noncomputable def cokernelIsoRangeQuotient {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    -- Porting note: broken dot notation
+    -- Porting note (#11036): broken dot notation
     cokernel f ≅ ModuleCat.of R (H ⧸ LinearMap.range f) :=
   colimit.isoColimitCocone ⟨_, cokernelIsColimit f⟩
 #align Module.cokernel_iso_range_quotient ModuleCat.cokernelIsoRangeQuotient

Mathlib/Algebra/Module/Torsion.lean

@@ -74,7 +74,7 @@ variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
 /-- The torsion ideal of `x`, containing all `a` such that `a • x = 0`.-/
 @[simps!]
 def torsionOf (x : M) : Ideal R :=
-  -- Porting note: broken dot notation on LinearMap.ker Lean4#1910
+  -- Porting note (#11036): broken dot notation on LinearMap.ker Lean4#1910
   LinearMap.ker (LinearMap.toSpanSingleton R M x)
 #align ideal.torsion_of Ideal.torsionOf
 
@@ -163,7 +163,7 @@ namespace Submodule
   `a • x = 0`. -/
 @[simps!]
 def torsionBy (a : R) : Submodule R M :=
-  -- Porting note: broken dot notation on LinearMap.ker Lean4#1910
+  -- Porting note (#11036): broken dot notation on LinearMap.ker Lean4#1910
   LinearMap.ker (DistribMulAction.toLinearMap R M a)
 #align submodule.torsion_by Submodule.torsionBy
 

Mathlib/LinearAlgebra/Dual.lean

@@ -369,12 +369,12 @@ theorem toDual_inj (m : M) (a : b.toDual m = 0) : m = 0 :=
   b.toDual_injective (by rwa [_root_.map_zero])
 #align basis.to_dual_inj Basis.toDual_inj
 
--- Porting note: broken dot notation lean4#1910 LinearMap.ker
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
 theorem toDual_ker : LinearMap.ker b.toDual = ⊥ :=
   ker_eq_bot'.mpr b.toDual_inj
 #align basis.to_dual_ker Basis.toDual_ker
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem toDual_range [Finite ι] : LinearMap.range b.toDual = ⊤ := by
   refine' eq_top_iff'.2 fun f => _
   let lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
@@ -491,7 +491,7 @@ theorem eval_ker {ι : Type*} (b : Basis ι R M) :
   exact (Basis.forall_coord_eq_zero_iff _).mp fun i => hm (b.coord i)
 #align basis.eval_ker Basis.eval_ker
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) :
     LinearMap.range (Dual.eval R M) = ⊤ := by
   classical
@@ -543,7 +543,7 @@ section
 
 variable (K) (V)
 
--- Porting note: broken dot notation lean4#1910 LinearMap.ker
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
 theorem eval_ker : LinearMap.ker (eval K V) = ⊥ := by
   classical exact (Module.Free.chooseBasis K V).eval_ker
 #align module.eval_ker Module.eval_ker
@@ -619,7 +619,7 @@ theorem dual_rank_eq [Module.Finite K V] :
   (Module.Free.chooseBasis K V).dual_rank_eq
 #align module.dual_rank_eq Module.dual_rank_eq
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem erange_coe [Module.Finite K V] : LinearMap.range (eval K V) = ⊤ :=
   (Module.Free.chooseBasis K V).eval_range
 #align module.erange_coe Module.erange_coe
@@ -902,7 +902,7 @@ theorem dualRestrict_apply (W : Submodule R M) (φ : Module.Dual R M) (x : W) :
   that `φ w = 0` for all `w ∈ W`. -/
 def dualAnnihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M]
     (W : Submodule R M) : Submodule R <| Module.Dual R M :=
--- Porting note: broken dot notation lean4#1910 LinearMap.ker
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
   LinearMap.ker W.dualRestrict
 #align submodule.dual_annihilator Submodule.dualAnnihilator
 
@@ -916,7 +916,7 @@ theorem mem_dualAnnihilator (φ : Module.Dual R M) : φ ∈ W.dualAnnihilator 
 /-- That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$.
 This is the definition of the dual annihilator of the submodule $W$. -/
 theorem dualRestrict_ker_eq_dualAnnihilator (W : Submodule R M) :
-    -- Porting note: broken dot notation lean4#1910 LinearMap.ker
+    -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
     LinearMap.ker W.dualRestrict = W.dualAnnihilator :=
   rfl
 #align submodule.dual_restrict_ker_eq_dual_annihilator Submodule.dualRestrict_ker_eq_dualAnnihilator
@@ -1171,7 +1171,7 @@ theorem quotAnnihilatorEquiv_apply (W : Subspace K V) (φ : Module.Dual K V) :
 #align subspace.quot_annihilator_equiv_apply Subspace.quotAnnihilatorEquiv_apply
 
 /-- The natural isomorphism from the dual of a subspace `W` to `W.dualLift.range`. -/
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 noncomputable def dualEquivDual (W : Subspace K V) :
     Module.Dual K W ≃ₗ[K] LinearMap.range W.dualLift :=
   LinearEquiv.ofInjective _ dualLift_injective
@@ -1216,7 +1216,7 @@ theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) :
 #align subspace.dual_annihilator_dual_annihilator_eq Subspace.dualAnnihilator_dualAnnihilator_eq
 
 /-- The quotient by the dual is isomorphic to its dual annihilator.  -/
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 noncomputable def quotDualEquivAnnihilator (W : Subspace K V) :
     (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] W.dualAnnihilator :=
   LinearEquiv.quotEquivOfQuotEquiv <| LinearEquiv.trans W.quotAnnihilatorEquiv W.dualEquivDual
@@ -1268,7 +1268,7 @@ variable [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M
 
 variable (f : M₁ →ₗ[R] M₂)
 
--- Porting note: broken dot notation lean4#1910 LinearMap.ker
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
 theorem ker_dualMap_eq_dualAnnihilator_range :
     LinearMap.ker f.dualMap = f.range.dualAnnihilator := by
   ext
@@ -1277,7 +1277,7 @@ theorem ker_dualMap_eq_dualAnnihilator_range :
   rfl
 #align linear_map.ker_dual_map_eq_dual_annihilator_range LinearMap.ker_dualMap_eq_dualAnnihilator_range
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem range_dualMap_le_dualAnnihilator_ker :
     LinearMap.range f.dualMap ≤ f.ker.dualAnnihilator := by
   rintro _ ⟨ψ, rfl⟩
@@ -1339,7 +1339,7 @@ theorem dualPairing_apply {W : Submodule R M} (φ : Module.Dual R M) (x : W) :
   rfl
 #align submodule.dual_pairing_apply Submodule.dualPairing_apply
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 /-- That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$. -/
 theorem range_dualMap_mkQ_eq (W : Submodule R M) :
     LinearMap.range W.mkQ.dualMap = W.dualAnnihilator := by
@@ -1362,7 +1362,7 @@ def dualQuotEquivDualAnnihilator (W : Submodule R M) :
     Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator :=
   LinearEquiv.ofLinear
     (W.mkQ.dualMap.codRestrict W.dualAnnihilator fun φ =>
--- Porting note: broken dot notation lean4#1910 LinearMap.mem_range_self
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.mem_range_self
       W.range_dualMap_mkQ_eq ▸ LinearMap.mem_range_self W.mkQ.dualMap φ)
     W.dualCopairing (by ext; rfl) (by ext; rfl)
 #align submodule.dual_quot_equiv_dual_annihilator Submodule.dualQuotEquivDualAnnihilator
@@ -1421,7 +1421,7 @@ namespace LinearMap
 
 open Submodule
 
--- Porting note: broken dot notation lean4#1910 LinearMap.range
+-- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem range_dualMap_eq_dualAnnihilator_ker_of_surjective (f : M →ₗ[R] M')
     (hf : Function.Surjective f) : LinearMap.range f.dualMap = f.ker.dualAnnihilator :=
   ((f.quotKerEquivOfSurjective hf).dualMap.range_comp _).trans f.ker.range_dualMap_mkQ_eq
@@ -1436,7 +1436,7 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M
     rw [← range_eq_top, range_rangeRestrict]
   have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
   convert this using 1
-  -- Porting note: broken dot notation lean4#1910
+  -- Porting note (#11036): broken dot notation lean4#1910
   · calc
       _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
       _ = _ := ?_
@@ -1479,7 +1479,7 @@ theorem dualMap_surjective_of_injective {f : V₁ →ₗ[K] V₂} (hf : Function
   ⟨φ.comp f', ext fun x ↦ congr(φ <| $hf' x)⟩
 #align linear_map.dual_map_surjective_of_injective LinearMap.dualMap_surjective_of_injective
 
-  -- Porting note: broken dot notation lean4#1910 LinearMap.range
+  -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.range
 theorem range_dualMap_eq_dualAnnihilator_ker (f : V₁ →ₗ[K] V₂) :
     LinearMap.range f.dualMap = f.ker.dualAnnihilator :=
   range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective f <|
@@ -1535,7 +1535,7 @@ theorem dualAnnihilator_inf_eq (W W' : Subspace K V₁) :
     (W ⊓ W').dualAnnihilator = W.dualAnnihilator ⊔ W'.dualAnnihilator := by
   refine' le_antisymm _ (sup_dualAnnihilator_le_inf W W')
   let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')
-  -- Porting note: broken dot notation lean4#1910 LinearMap.ker
+  -- Porting note (#11036): broken dot notation lean4#1910 LinearMap.ker
   have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]
   rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
   intro φ
@@ -1594,7 +1594,7 @@ namespace LinearMap
 
 @[simp]
 theorem finrank_range_dualMap_eq_finrank_range (f : V₁ →ₗ[K] V₂) :
-    -- Porting note: broken dot notation lean4#1910
+    -- Porting note (#11036): broken dot notation lean4#1910
     finrank K (LinearMap.range f.dualMap) = finrank K (LinearMap.range f) := by
   rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl),
     ← dualMap_comp_dualMap, range_comp,

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -239,7 +239,7 @@ def toGL : SpecialLinearGroup n R →* GeneralLinearGroup R (n → R) :=
 set_option linter.uppercaseLean3 false in
 #align matrix.special_linear_group.to_GL Matrix.SpecialLinearGroup.toGL
 
--- Porting note: broken dot notation
+-- Porting note (#11036): broken dot notation
 theorem coe_toGL (A : SpecialLinearGroup n R) : SpecialLinearGroup.toGL A = A.toLin'.toLinearMap :=
   rfl
 set_option linter.uppercaseLean3 false in