Commit 2021-10-04 09:48 abe81bcb

View on Github →

feat(linear_algebra/matrix/general_linear_group): GL(n, R) (#8466) added this file which contains definition of the general linear group as well as the subgroup of matrices with positive determinant.

Estimated changes

Created src/linear_algebra/general_linear_group.lean

added def matrix.GL_pos

added theorem matrix.GL_pos_coe_neg

added theorem matrix.GL_pos_neg_elt

added theorem matrix.general_linear_group.coe_fn_eq_coe

added theorem matrix.general_linear_group.coe_inv

added theorem matrix.general_linear_group.coe_mul

added theorem matrix.general_linear_group.coe_one

added def matrix.general_linear_group.det

added theorem matrix.general_linear_group.ext

added theorem matrix.general_linear_group.ext_iff

added def matrix.general_linear_group.mk'

added def matrix.general_linear_group.to_lin

added def matrix.general_linear_group

added theorem matrix.mem_GL_pos

added theorem matrix.special_linear_group.coe_eq_to_GL_pos

added def matrix.special_linear_group.to_GL_pos

added theorem matrix.special_linear_group.to_GL_pos_injective

Modified src/ring_theory/subring.lean

added theorem units.mem_pos_subgroup

added def units.pos_subgroup

Modified src/ring_theory/subsemiring.lean

added theorem mem_pos_monoid

added def pos_submonoid