diff --git a/LeanPool/CompositionAlgebrasOverRings/Composition/ComplexQuaternion.lean b/LeanPool/CompositionAlgebrasOverRings/Composition/ComplexQuaternion.lean
index 36812f854..f35caf522 100644
--- a/LeanPool/CompositionAlgebrasOverRings/Composition/ComplexQuaternion.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/Composition/ComplexQuaternion.lean
@@ -108,9 +108,9 @@ unify. So the conjugation is only ever rewritten through its **components**, and
 `cay_conj_apply` is removed from the default simp set with `-cay_conj_apply`.
 
 The second is that `ℍ[ℝ]` is a `def` wrapping `QuaternionAlgebra ℝ (-1) 0 (-1)`. A goal mixing
-that spelling with `RealQuaternion` is not type-correct at `rw`'s transparency, so all quaternion
-arithmetic is done in `ConicAlgebra.quaternion_mk_mul` and `ConicAlgebra.quaternion_star_mk`,
-whose statements mention no `Cay`, and then used as fully instantiated rewrites. -/
+that spelling with `RealQuaternion` is not type-correct at `rw`'s transparency, so each quaternion
+computation first `change`s its goal into the `ℍ[ℝ, -1, 0, -1]` spelling and only then rewrites
+with `QuaternionAlgebra.mk_mul_mk` or `QuaternionAlgebra.star_mk`. -/
 
 private theorem cay₂_conj_fst (μ : ℝ) (x : Cay₂ ℝ μ) :
     ((cay₂ ℝ μ).conj x).1 = x.1 := by
@@ -128,20 +128,6 @@ private theorem cay₄_conj_snd (x : RealQuaternion) :
     ((cay₄ ℝ (-1) (-1)).conj x).2 = -x.2 := by
   rw [cay_conj_apply]
 
-private theorem quaternion_mk_mul (a₁ b₁ c₁ d₁ a₂ b₂ c₂ d₂ : ℝ) :
-    (⟨a₁, b₁, c₁, d₁⟩ : ℍ[ℝ]) * ⟨a₂, b₂, c₂, d₂⟩ =
-      ⟨a₁ * a₂ - b₁ * b₂ - c₁ * c₂ - d₁ * d₂,
-        a₁ * b₂ + b₁ * a₂ + c₁ * d₂ - d₁ * c₂,
-        a₁ * c₂ - b₁ * d₂ + c₁ * a₂ + d₁ * b₂,
-        a₁ * d₂ + b₁ * c₂ - c₁ * b₂ + d₁ * a₂⟩ := by
-  rw [QuaternionAlgebra.mk_mul_mk, QuaternionAlgebra.mk.injEq]
-  exact ⟨by ring, by ring, by ring, by ring⟩
-
-private theorem quaternion_star_mk (a b c d : ℝ) :
-    star (⟨a, b, c, d⟩ : ℍ[ℝ]) = ⟨a, -b, -c, -d⟩ := by
-  rw [QuaternionAlgebra.star_mk, QuaternionAlgebra.mk.injEq]
-  exact ⟨by ring, rfl, rfl, rfl⟩
-
 /-- The underlying map `((a, b), (c, d)) ↦ a + bi + cj + dk`. -/
 def toQuaternion (x : RealQuaternion) : ℍ[ℝ] := ⟨x.1.1, x.1.2, x.2.1, x.2.2⟩
 
diff --git a/LeanPool/CompositionAlgebrasOverRings/Composition/RankDichotomy.lean b/LeanPool/CompositionAlgebrasOverRings/Composition/RankDichotomy.lean
index 86905d3bd..08d428af7 100644
--- a/LeanPool/CompositionAlgebrasOverRings/Composition/RankDichotomy.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/Composition/RankDichotomy.lean
@@ -171,17 +171,9 @@ theorem eq_unitForm_smul_one_of_rankAtStalk_eq_one (D : ConicAlgebra k B)
     [Nontrivial k] (hB : Module.rankAtStalk (R := k) B = fun _ ↦ 1) (x : B) :
     x = D.unitForm x • (1 : B) := by
   let N := LinearMap.ker D.unitForm
-  let p : B →ₗ[k] N := LinearMap.codRestrict N
-    (LinearMap.id - LinearMap.toSpanSingleton k B 1 ∘ₗ D.unitForm) (fun z ↦ by
-      simp [N, LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, D.unitForm_one])
-  have hpi : p ∘ₗ N.subtype = LinearMap.id := by
-    refine LinearMap.ext fun z ↦ Subtype.ext ?_
-    have hz : D.unitForm (z : B) = 0 := z.2
-    simp [p, hz, LinearMap.toSpanSingleton_apply]
-  let : Module.Finite k N :=
-    Module.Finite.of_surjective p fun z ↦ ⟨(z : B), DFunLike.congr_fun hpi z⟩
-  let : Module.Projective k N := Module.Projective.of_split N.subtype p hpi
   let E := LinearMap.equivProdKerOfApplyEqOne D.unitForm (1 : B) D.unitForm_one
+  have : Module.Finite k N := .of_linearEquiv_prod E
+  have : Module.Projective k N := .of_linearEquiv_prod E
   have hN : Module.rankAtStalk (R := k) N = 0 := by
     have hprod := Module.rankAtStalk_prod (R := k) k N
     have hE := Module.rankAtStalk_eq_of_equiv E
diff --git a/LeanPool/CompositionAlgebrasOverRings/Composition/Reduced/Classification.lean b/LeanPool/CompositionAlgebrasOverRings/Composition/Reduced/Classification.lean
index 13a09a740..111df6214 100644
--- a/LeanPool/CompositionAlgebrasOverRings/Composition/Reduced/Classification.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/Composition/Reduced/Classification.lean
@@ -125,6 +125,12 @@ theorem ProjectiveConstantRankFree.of_isLGRing (hLG : IsLGRing k) :
     ProjectiveConstantRankFree.{u, w} k :=
   fun M _ _ _ _ r hM ↦ Module.free_of_isLGRing_of_rankAtStalk_eq hLG r M hM
 
+/-- Over a PID every finitely generated projective module is free, being torsion-free, so
+`GPR`'s freeness hypothesis holds; this is the freeness step of `GPR 22.19`. -/
+theorem ProjectiveConstantRankFree.of_isPrincipalIdealRing [IsDomain k] [IsPrincipalIdealRing k] :
+    ProjectiveConstantRankFree.{u, w} k :=
+  fun _ _ _ _ _ _ _ ↦ Module.free_of_finite_type_torsion_free'
+
 private theorem finrank_eq_of_rankAtStalk_eq [Nontrivial k]
     {M : Type v} [AddCommGroup M] [Module k M] [Module.Free k M]
     (hM : Module.rankAtStalk (R := k) M = fun _ ↦ n) : Module.finrank k M = n := by
@@ -145,25 +151,6 @@ theorem isSplitOfRank_two (hc : C.IsElementaryIdempotent c)
       hc.splitEtaleEquiv_one hA, hc.splitEtaleEquiv_mul hA⟩
   exact hiso.symm
 
-/-- **`GPR 22.16`, rank four:** over a nontrivial LG ring, a reduced constant-rank-four
-composition algebra is split. -/
-theorem isSplitOfRank_four_of_isLGRing [Nontrivial k]
-    (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k)
-    (hcomp : C.IsComposition.{u, v, u})
-    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 4) : C.IsSplitOfRank 4 := by
-  let L := TwistingModule (k := k) c
-  let : Module.Finite k L := IsAlternative.finite_peirceComponent true false
-  let : Module.Projective k L :=
-    IsAlternative.projective_peirceComponent hc.mul_self true false
-  have hL : Module.rankAtStalk (R := k) L = 1 :=
-    hc.rankAtStalk_offDiagonal_eq_one hcomp.isMultiplicative
-      (hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)) hA true
-  let : Module.Free k L := Module.free_of_isLGRing_of_rankAtStalk_eq hLG 1 L hL
-  let b : Module.Basis Unit k L :=
-    Module.basisUnique Unit (finrank_eq_of_rankAtStalk_eq hL)
-  exact (hc.isomorphic_twistedMat (k := k) hcomp hA).symm.trans
-    (isomorphic_twistedMat_ofBasis k b)
-
 /-- **`GPR 22.16`, rank four under its abstract freeness hypothesis.** -/
 theorem isSplitOfRank_four_of_projective_constantRank_free [Nontrivial k]
     (hc : C.IsElementaryIdempotent c)
@@ -184,45 +171,23 @@ theorem isSplitOfRank_four_of_projective_constantRank_free [Nontrivial k]
   exact (hc.isomorphic_twistedMat (k := k) hcomp hA).symm.trans
     (isomorphic_twistedMat_ofBasis k b)
 
+/-- **`GPR 22.16`, rank four:** over a nontrivial LG ring, a reduced constant-rank-four
+composition algebra is split. -/
+theorem isSplitOfRank_four_of_isLGRing [Nontrivial k]
+    (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k)
+    (hcomp : C.IsComposition.{u, v, u})
+    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 4) : C.IsSplitOfRank 4 :=
+  hc.isSplitOfRank_four_of_projective_constantRank_free
+    (ProjectiveConstantRankFree.of_isLGRing hLG) hcomp hA
+
 /-- **`GPR 22.19`, rank four:** over a PID, a reduced constant-rank-four composition algebra is
 split. The twisting line is projective, hence flat and torsion-free, and a finite torsion-free
 module over a PID is free. -/
 theorem isSplitOfRank_four_of_pid [IsDomain k] [IsPrincipalIdealRing k]
     (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition.{u, v, u})
-    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 4) : C.IsSplitOfRank 4 := by
-  let L := TwistingModule (k := k) c
-  let : Module.Finite k L := IsAlternative.finite_peirceComponent true false
-  let : Module.Projective k L :=
-    IsAlternative.projective_peirceComponent hc.mul_self true false
-  let : Module.IsTorsionFree k L := inferInstance
-  let : Module.Free k L := Module.free_of_finite_type_torsion_free'
-  have hL : Module.rankAtStalk (R := k) L = 1 :=
-    hc.rankAtStalk_offDiagonal_eq_one hcomp.isMultiplicative
-      (hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)) hA true
-  let b : Module.Basis Unit k L :=
-    Module.basisUnique Unit (finrank_eq_of_rankAtStalk_eq hL)
-  exact (hc.isomorphic_twistedMat (k := k) hcomp hA).symm.trans
-    (isomorphic_twistedMat_ofBasis k b)
-
-/-- **`GPR 22.16`, rank eight:** over a nontrivial LG ring, a reduced constant-rank-eight
-composition algebra is split. -/
-theorem isSplitOfRank_eight_of_isLGRing [Nontrivial k]
-    (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k)
-    (hcomp : C.IsComposition.{u, v, u})
-    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 8) : C.IsSplitOfRank 8 := by
-  let M := ZornTwistingModule (k := k) c
-  let : Module.Finite k M := IsAlternative.finite_peirceComponent true false
-  let : Module.Projective k M :=
-    IsAlternative.projective_peirceComponent hc.mul_self true false
-  let hreg := hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)
-  let P := hc.peirceVectorProductPair hcomp.isMultiplicative hreg
-  have hM : Module.rankAtStalk (R := k) M = 3 :=
-    hc.rankAtStalk_twistingModule_eq_three hcomp.isMultiplicative hreg hA
-  let : Module.Free k M := Module.free_of_isLGRing_of_rankAtStalk_eq hLG 3 M hM
-  let b : Module.Basis (Fin 3) k M :=
-    Module.finBasisOfFinrankEq k M (finrank_eq_of_rankAtStalk_eq hM)
-  exact (hc.isomorphic_twistedZor (k := k) hcomp.isMultiplicative hreg).symm.trans
-    (isomorphic_twistedZor_of_exists_basis P b)
+    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 4) : C.IsSplitOfRank 4 :=
+  hc.isSplitOfRank_four_of_projective_constantRank_free
+    ProjectiveConstantRankFree.of_isPrincipalIdealRing hcomp hA
 
 /-- **`GPR 22.16`, rank eight under its abstract freeness hypothesis.** -/
 theorem isSplitOfRank_eight_of_projective_constantRank_free [Nontrivial k]
@@ -246,25 +211,22 @@ theorem isSplitOfRank_eight_of_projective_constantRank_free [Nontrivial k]
   exact (hc.isomorphic_twistedZor (k := k) hcomp.isMultiplicative hreg).symm.trans
     (isomorphic_twistedZor_of_exists_basis P b)
 
+/-- **`GPR 22.16`, rank eight:** over a nontrivial LG ring, a reduced constant-rank-eight
+composition algebra is split. -/
+theorem isSplitOfRank_eight_of_isLGRing [Nontrivial k]
+    (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k)
+    (hcomp : C.IsComposition.{u, v, u})
+    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 8) : C.IsSplitOfRank 8 :=
+  hc.isSplitOfRank_eight_of_projective_constantRank_free
+    (ProjectiveConstantRankFree.of_isLGRing hLG) hcomp hA
+
 /-- **`GPR 22.19`, rank eight:** over a PID, a reduced constant-rank-eight composition algebra is
 split. The rank-three twisting module is projective, hence finite free over the PID. -/
 theorem isSplitOfRank_eight_of_pid [IsDomain k] [IsPrincipalIdealRing k]
     (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition.{u, v, u})
-    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 8) : C.IsSplitOfRank 8 := by
-  let M := ZornTwistingModule (k := k) c
-  let : Module.Finite k M := IsAlternative.finite_peirceComponent true false
-  let : Module.Projective k M :=
-    IsAlternative.projective_peirceComponent hc.mul_self true false
-  let : Module.IsTorsionFree k M := inferInstance
-  let : Module.Free k M := Module.free_of_finite_type_torsion_free'
-  let hreg := hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)
-  let P := hc.peirceVectorProductPair hcomp.isMultiplicative hreg
-  have hM : Module.rankAtStalk (R := k) M = 3 :=
-    hc.rankAtStalk_twistingModule_eq_three hcomp.isMultiplicative hreg hA
-  let b : Module.Basis (Fin 3) k M :=
-    Module.finBasisOfFinrankEq k M (finrank_eq_of_rankAtStalk_eq hM)
-  exact (hc.isomorphic_twistedZor (k := k) hcomp.isMultiplicative hreg).symm.trans
-    (isomorphic_twistedZor_of_exists_basis P b)
+    (hA : Module.rankAtStalk (R := k) A = fun _ ↦ 8) : C.IsSplitOfRank 8 :=
+  hc.isSplitOfRank_eight_of_projective_constantRank_free
+    ProjectiveConstantRankFree.of_isPrincipalIdealRing hcomp hA
 
 end IsElementaryIdempotent
 
@@ -425,21 +387,8 @@ reverse implication uses `GPR 22.9` and the reduced classification of `GPR 22.16
 theorem isSplitOfRank_iff_isGPRIsotropic_of_isLGRing [Nontrivial k]
     (hcomp : C.IsComposition.{u, v, u}) (hLG : IsLGRing k)
     (hA : Module.rankAtStalk (R := k) A = fun _ ↦ r)
-    (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ C.norm.IsGPRIsotropic := by
-  constructor
-  · intro hsplit
-    obtain ⟨c, hc⟩ := hsplit.hasElementaryIdempotent_of_two_or_four_or_eight hr
-    exact hc.isGPRIsotropic
-  · intro hiso
-    have hreg := hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)
-    obtain ⟨c, hc⟩ := exists_isElementaryIdempotent_of_isGPRIsotropic
-      hreg hcomp.isMultiplicative hiso
-    let : IsAlternative A :=
-      hcomp.isMultiplicative.isAlternative hreg.isGPRNondegenerate
-    rcases hr with rfl | rfl | rfl
-    · exact hc.isSplitOfRank_two hA
-    · exact hc.isSplitOfRank_four_of_isLGRing hLG hcomp hA
-    · exact hc.isSplitOfRank_eight_of_isLGRing hLG hcomp hA
+    (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ C.norm.IsGPRIsotropic :=
+  hcomp.isSplitOfRank_iff_isGPRIsotropic_of_projectiveConstantRankFree (.of_isLGRing hLG) hA hr
 
 omit [IsAlternative A] in
 /-- **`GPR 22.18`, hyperbolic ⇒ split over an LG ring.** A norm isometric to a hyperbolic form
@@ -474,21 +423,9 @@ twisting modules are free over the PID, replacing the LG-ring freeness step in `
 theorem isSplitOfRank_iff_isGPRIsotropic_of_pid [IsDomain k] [IsPrincipalIdealRing k]
     (hcomp : C.IsComposition.{u, v, u})
     (hA : Module.rankAtStalk (R := k) A = fun _ ↦ r)
-    (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ C.norm.IsGPRIsotropic := by
-  constructor
-  · intro hsplit
-    obtain ⟨c, hc⟩ := hsplit.hasElementaryIdempotent_of_two_or_four_or_eight hr
-    exact hc.isGPRIsotropic
-  · intro hiso
-    have hreg := hcomp.isGPRRegular_of_rankAtStalk_ne_one hA (by omega)
-    obtain ⟨c, hc⟩ := exists_isElementaryIdempotent_of_isGPRIsotropic
-      hreg hcomp.isMultiplicative hiso
-    let : IsAlternative A :=
-      hcomp.isMultiplicative.isAlternative hreg.isGPRNondegenerate
-    rcases hr with rfl | rfl | rfl
-    · exact hc.isSplitOfRank_two hA
-    · exact hc.isSplitOfRank_four_of_pid hcomp hA
-    · exact hc.isSplitOfRank_eight_of_pid hcomp hA
+    (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ C.norm.IsGPRIsotropic :=
+  hcomp.isSplitOfRank_iff_isGPRIsotropic_of_projectiveConstantRankFree
+    .of_isPrincipalIdealRing hA hr
 
 omit [IsAlternative A] in
 /-- **`GPR 22.19`, split ↔ a nonzero null vector over a PID.** This is where GPR's
diff --git a/LeanPool/CompositionAlgebrasOverRings/Conic/Projective.lean b/LeanPool/CompositionAlgebrasOverRings/Conic/Projective.lean
index af803c97e..bbacaeb28 100644
--- a/LeanPool/CompositionAlgebrasOverRings/Conic/Projective.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/Conic/Projective.lean
@@ -129,16 +129,9 @@ theorem norm_eq_of_projective (C D : ConicAlgebra k A) : C.norm = D.norm := by
     simp only [map_smul, C.unitForm_one, smul_eq_mul, mul_one] at h
     exact h.symm
   set N : Submodule k A := LinearMap.ker C.unitForm with hN
-  set p : A →ₗ[k] N := LinearMap.codRestrict N
-    (LinearMap.id - LinearMap.toSpanSingleton k A 1 ∘ₗ C.unitForm) (fun z ↦ by
-      simp [hN, LinearMap.mem_ker, LinearMap.toSpanSingleton_apply]) with hp
-  have hpi : p ∘ₗ N.subtype = LinearMap.id := by
-    refine LinearMap.ext fun z ↦ Subtype.ext ?_
-    have hz : C.unitForm (z : A) = 0 := z.2
-    simp [hp, hz, LinearMap.toSpanSingleton_apply]
-  have : Module.Finite k N :=
-    Module.Finite.of_surjective p fun z ↦ ⟨(z : A), DFunLike.congr_fun hpi z⟩
-  have : Module.Projective k N := Module.Projective.of_split N.subtype p hpi
+  let e := LinearMap.equivProdKerOfApplyEqOne C.unitForm 1 C.unitForm_one
+  have : Module.Finite k N := .of_linearEquiv_prod e
+  have : Module.Projective k N := .of_linearEquiv_prod e
   have hdN : d.comp N.subtype = 0 := by
     refine LinearMap.eq_zero_of_smul_self_eq_zero _ fun z ↦ ?_
     refine Subtype.ext ?_
@@ -190,16 +183,9 @@ conic algebra over `ℤ/4`, on a non-projective module, whose trace defect is `2
 theorem traceDefect_eq_zero_of_projective (x y : A) : C.traceDefect x y = 0 := by
   -- the kernel of `λ`, a direct summand of `A` and so finitely generated projective
   set N : Submodule k A := LinearMap.ker C.unitForm with hN
-  set p : A →ₗ[k] N := LinearMap.codRestrict N (LinearMap.id - (LinearMap.toSpanSingleton k A 1)
-    ∘ₗ C.unitForm) (fun z ↦ by
-      simp [hN, LinearMap.mem_ker, LinearMap.toSpanSingleton_apply]) with hp
-  have hpi : p ∘ₗ N.subtype = LinearMap.id := by
-    refine LinearMap.ext fun z ↦ Subtype.ext ?_
-    have hz : C.unitForm (z : A) = 0 := z.2
-    simp [hp, hz, LinearMap.toSpanSingleton_apply]
-  have : Module.Finite k N :=
-    Module.Finite.of_surjective p fun z ↦ ⟨(z : A), DFunLike.congr_fun hpi z⟩
-  have : Module.Projective k N := Module.Projective.of_split N.subtype p hpi
+  let e := LinearMap.equivProdKerOfApplyEqOne C.unitForm 1 C.unitForm_one
+  have : Module.Finite k N := .of_linearEquiv_prod e
+  have : Module.Projective k N := .of_linearEquiv_prod e
   -- the trace defect restricted to `N` annihilates its own argument
   have hzero : (C.traceDefectLeft y).comp N.subtype = 0 := by
     refine LinearMap.eq_zero_of_smul_self_eq_zero _ fun z ↦ ?_
diff --git a/LeanPool/CompositionAlgebrasOverRings/LGRing/ConstantRank.lean b/LeanPool/CompositionAlgebrasOverRings/LGRing/ConstantRank.lean
index 42ad6cbbc..f396df40f 100644
--- a/LeanPool/CompositionAlgebrasOverRings/LGRing/ConstantRank.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/LGRing/ConstantRank.lean
@@ -66,20 +66,6 @@ open scoped TensorProduct
 
 variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
 
-/-- A module that splits off a free rank-one summand from a finitely generated module is itself
-finitely generated. -/
-theorem Module.Finite.of_linearEquiv_prod {N : Type v} [AddCommGroup N] [Module R N]
-    [Module.Finite R M] (e : M ≃ₗ[R] R × N) : Module.Finite R N :=
-  haveI : Module.Finite R (R × N) := Module.Finite.equiv e
-  Module.Finite.of_surjective (LinearMap.snd R R N) Prod.snd_surjective
-
-/-- A module that splits off a free rank-one summand from a projective module is itself
-projective. -/
-theorem Module.Projective.of_linearEquiv_prod {N : Type v} [AddCommGroup N] [Module R N]
-    [Module.Projective R M] (e : M ≃ₗ[R] R × N) : Module.Projective R N :=
-  haveI : Module.Projective R (R × N) := Module.Projective.of_equiv' e
-  Module.Projective.of_split (LinearMap.inr R R N) (LinearMap.snd R R N) (by ext x; simp)
-
 /-- Positive rank at a maximal ideal makes the residue-field fibre nonzero.
 
 This is the bridge from `Module.rankAtStalk`, which is defined through the localization `R_𝔪`, to
diff --git a/LeanPool/CompositionAlgebrasOverRings/Module/Unimodular.lean b/LeanPool/CompositionAlgebrasOverRings/Module/Unimodular.lean
index b93cbedd1..118a866b3 100644
--- a/LeanPool/CompositionAlgebrasOverRings/Module/Unimodular.lean
+++ b/LeanPool/CompositionAlgebrasOverRings/Module/Unimodular.lean
@@ -38,6 +38,8 @@ This is not a norm-theoretic notion — no quadratic form is in sight here — b
   vector in a vector space is hit by a functional. This is what collapses GPR-sense isotropy onto
   mathlib's `Anisotropic` over a field; see `QuadraticForm/Isotropic.lean`.
 * `Module.IsUnimodular.exists_linearEquiv_prod` : a unimodular element splits `M` as `R × M'`.
+* `Module.Finite.of_linearEquiv_prod`, `Module.Projective.of_linearEquiv_prod` : the complement
+  `M'` of such a splitting is finitely generated, resp. projective, when `M` is.
 
 ## Implementation notes
 
@@ -179,3 +181,17 @@ theorem Module.IsUnimodular.exists_linearEquiv_prod {m : M} (hm : Module.IsUnimo
     ∃ M' : Submodule R M, Nonempty (M ≃ₗ[R] R × M') := by
   obtain ⟨l, hl⟩ := Module.isUnimodular_iff.mp hm
   exact ⟨LinearMap.ker l, ⟨LinearMap.equivProdKerOfApplyEqOne l m hl⟩⟩
+
+/-- A module that splits off a free rank-one summand from a finitely generated module is itself
+finitely generated. -/
+theorem Module.Finite.of_linearEquiv_prod {N : Type v} [AddCommGroup N] [Module R N]
+    [Module.Finite R M] (e : M ≃ₗ[R] R × N) : Module.Finite R N :=
+  haveI : Module.Finite R (R × N) := Module.Finite.equiv e
+  Module.Finite.of_surjective (LinearMap.snd R R N) Prod.snd_surjective
+
+/-- A module that splits off a free rank-one summand from a projective module is itself
+projective. -/
+theorem Module.Projective.of_linearEquiv_prod {N : Type v} [AddCommGroup N] [Module R N]
+    [Module.Projective R M] (e : M ≃ₗ[R] R × N) : Module.Projective R N :=
+  haveI : Module.Projective R (R × N) := Module.Projective.of_equiv' e
+  Module.Projective.of_split (LinearMap.inr R R N) (LinearMap.snd R R N) (by ext x; simp)