feat: port LinearAlgebra.Prod (#2415)

leanprover-community · Feb 21, 2023 · 05d37dd · 05d37dd
1 parent 628f140
commit 05d37dd
Show file tree

Hide file tree

Showing 5 changed files with 1,020 additions and 4 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -830,6 +830,7 @@ import Mathlib.LinearAlgebra.Basic
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.Pi
+import Mathlib.LinearAlgebra.Prod
 import Mathlib.LinearAlgebra.Quotient
 import Mathlib.LinearAlgebra.Span
 import Mathlib.Logic.Basic

diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
@@ -40,10 +40,10 @@ structure AlgHom (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiri
 /-- Reinterpret an `AlgHom` as a `RingHom` -/
 add_decl_doc AlgHom.toRingHom
 
--- mathport name: «expr →ₐ »
+@[inherit_doc AlgHom]
 infixr:25 " →ₐ " => AlgHom _
 
--- mathport name: «expr →ₐ[ ] »
+@[inherit_doc]
 notation:25 A " →ₐ[" R "] " B => AlgHom R A B
 
 /-- `AlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms

diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean
@@ -55,6 +55,8 @@ structure LinearEquiv {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ :
   [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap σ M M₂, M ≃+ M₂
 #align linear_equiv LinearEquiv
 
+attribute [coe] LinearEquiv.toLinearMap
+
 /-- The linear map underlying a linear equivalence. -/
 add_decl_doc LinearEquiv.toLinearMap
 #align linear_equiv.to_linear_map LinearEquiv.toLinearMap

diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean
@@ -557,8 +557,6 @@ infixr:80 " ∘ₗ " =>
   @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _)
     RingHomCompTriple.ids
 
-include σ₁₃
-
 theorem comp_apply (x : M₁) : f.comp g x = f (g x) :=
   rfl
 #align linear_map.comp_apply LinearMap.comp_apply