Commit 2023-02-03 10:29 afdc959a

View on Github →

feat: port LinearAlgebra.GeneralLinearGroup (#2035)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/GeneralLinearGroup.lean

added theorem LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv

added def LinearMap.GeneralLinearGroup.generalLinearEquiv

added theorem LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap

added def LinearMap.GeneralLinearGroup.ofLinearEquiv

added def LinearMap.GeneralLinearGroup.toLinearEquiv

added def LinearMap.GeneralLinearGroup