Commit 2024-06-15 21:43 0e39a68f

View on Github →

A ring homomorphism f : R →+* S induces a homomorphism GLₙ(f) : GLₙ(R) →* GLₙ(S). (#13768)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

added def Matrix.GeneralLinearGroup.map

added theorem Matrix.GeneralLinearGroup.map_comp

added theorem Matrix.GeneralLinearGroup.map_comp_apply

added theorem Matrix.GeneralLinearGroup.map_id