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