Theorem Matrix.GeneralLinearGroup.map_id

Modification history

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.map_idView on Github →