Commit 2023-02-01 12:38 ae690b0c

View on Github →

refactor(linear_algebra/{general,special}_linear_group): move to matrix subfolder (#18344) This frees up linear_algebra/general_linear_group to be about linear_map.general_linear_group.

Estimated changes

Modified src/analysis/complex/isometry.lean

Modified src/analysis/complex/upper_half_plane/basic.lean

Renamed src/linear_algebra/general_linear_group.lean to src/linear_algebra/matrix/general_linear_group.lean

Renamed src/linear_algebra/special_linear_group.lean to src/linear_algebra/matrix/special_linear_group.lean

Modified src/number_theory/modular.lean

Modified src/number_theory/modular_forms/congruence_subgroups.lean

Modified src/number_theory/modular_forms/slash_actions.lean