Commit 2023-05-18 07:35 0fe136b3

View on Github →

feat: port LinearAlgebra.UnitaryGroup (#3699) I use name unitaryGroup (because it's a Submonoid, not a Type _) and namespace UnitaryGroup. Should I change either of these names? Also, I don't know how to fix the timeout in the simpNF linter.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/UnitaryGroup.lean

added theorem Matrix.UnitaryGroup.coe_toGL

added def Matrix.UnitaryGroup.embeddingGL

added theorem Matrix.UnitaryGroup.ext

added theorem Matrix.UnitaryGroup.ext_iff

added theorem Matrix.UnitaryGroup.inv_apply

added theorem Matrix.UnitaryGroup.inv_val

added theorem Matrix.UnitaryGroup.mul_apply

added theorem Matrix.UnitaryGroup.mul_val

added theorem Matrix.UnitaryGroup.one_apply

added theorem Matrix.UnitaryGroup.one_val

added theorem Matrix.UnitaryGroup.star_mul_self

added def Matrix.UnitaryGroup.toGL

added theorem Matrix.UnitaryGroup.toGL_mul

added theorem Matrix.UnitaryGroup.toGL_one

added def Matrix.UnitaryGroup.toLin'

added theorem Matrix.UnitaryGroup.toLin'_mul

added theorem Matrix.UnitaryGroup.toLin'_one

added def Matrix.UnitaryGroup.toLinearEquiv

added theorem Matrix.det_of_mem_unitary

added theorem Matrix.mem_orthogonalGroup_iff'

added theorem Matrix.mem_orthogonalGroup_iff

added theorem Matrix.mem_unitaryGroup_iff'

added theorem Matrix.mem_unitaryGroup_iff