Theorem LinearMap.toAddMonoidHom_proj

Modification history

2026-10-27 00:37

Mathlib/Algebra/Module/Pi.lean

chore(Algebra): move `LinearMap.proj` and `LinearMap.pi` (#45302) …

Modified LinearMap.toAddMonoidHom_proj View on Github →

2025-08-04 21:54

Mathlib/LinearAlgebra/Pi.lean

feat: add naming hint to doc string of `LinearMap.proj` (#27685) …

Added LinearMap.toAddMonoidHom_proj View on Github →