Def SpecialLinearGroup.toGeneralLinearGroup

Modification history

2025-11-16 15:54

Mathlib/LinearAlgebra/SpecialLinearGroup.lean

feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module (#30987) …

Added SpecialLinearGroup.toGeneralLinearGroup View on Github →