Def Matrix.GeneralLinearGroup.map

Modification history

2026-09-22 14:39
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
chore: remove redundant `<|` (#44067) …
Modified Matrix.GeneralLinearGroup.mapView on Github →
2024-06-15 21:43
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean
A ring homomorphism ``f : R →+* S`` induces a homomorphism ``GLₙ(f) : GLₙ(R) →* GLₙ(S)``. (#13768)
Added Matrix.GeneralLinearGroup.mapView on Github →