Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-15 13:26 0fa13128

View on Github →

feat(linear_algebra/unitary_group): add unitary/orthogonal groups (#5702)

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.star_mul

Created src/linear_algebra/unitary_group.lean

added def matrix.orthogonal_group

added theorem matrix.unitary_group.coe_to_GL

added def matrix.unitary_group.embedding_GL

added theorem matrix.unitary_group.ext

added theorem matrix.unitary_group.ext_iff

added theorem matrix.unitary_group.inv_apply

added theorem matrix.unitary_group.inv_val

added theorem matrix.unitary_group.mul_apply

added theorem matrix.unitary_group.mul_val

added theorem matrix.unitary_group.one_apply

added theorem matrix.unitary_group.one_val

added theorem matrix.unitary_group.star_mul_self

added def matrix.unitary_group.to_GL

added theorem matrix.unitary_group.to_GL_mul

added theorem matrix.unitary_group.to_GL_one

added def matrix.unitary_group.to_lin'

added theorem matrix.unitary_group.to_lin'_mul

added theorem matrix.unitary_group.to_lin'_one

added def matrix.unitary_group.to_linear_equiv

added def matrix.unitary_group

added theorem matrix.unitary_submonoid.star_mem

added theorem matrix.unitary_submonoid.star_mem_iff

added def unitary_submonoid