Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-02-02 17:00
2705404e
View on Github →
refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (
#18345
)
Estimated changes
Modified
src/linear_algebra/affine_space/affine_equiv.lean
Modified
src/linear_algebra/basic.lean
deleted
theorem
linear_map.general_linear_group.coe_fn_general_linear_equiv
deleted
def
linear_map.general_linear_group.general_linear_equiv
deleted
theorem
linear_map.general_linear_group.general_linear_equiv_to_linear_map
deleted
def
linear_map.general_linear_group.of_linear_equiv
deleted
def
linear_map.general_linear_group.to_linear_equiv
deleted
def
linear_map.general_linear_group
Modified
src/linear_algebra/determinant.lean
Modified
src/linear_algebra/eigenspace.lean
Created
src/linear_algebra/general_linear_group.lean
added
theorem
linear_map.general_linear_group.coe_fn_general_linear_equiv
added
def
linear_map.general_linear_group.general_linear_equiv
added
theorem
linear_map.general_linear_group.general_linear_equiv_to_linear_map
added
def
linear_map.general_linear_group.of_linear_equiv
added
def
linear_map.general_linear_group.to_linear_equiv
added
def
linear_map.general_linear_group
Modified
src/linear_algebra/matrix/general_linear_group.lean
Modified
src/linear_algebra/matrix/special_linear_group.lean
Modified
src/linear_algebra/unitary_group.lean
Modified
src/number_theory/modular.lean