Commit 2025-07-15 08:11 341594fa

View on Github →

feat: characterise membership in SO(2) (#27121) Also rename the ring from β to R because that's a really weird name for a ring. From Toric

Estimated changes

Modified Mathlib/LinearAlgebra/UnitaryGroup.lean

modified theorem Matrix.mem_orthogonalGroup_iff'

modified theorem Matrix.mem_orthogonalGroup_iff

added theorem Matrix.mem_specialOrthogonalGroup_fin_two_iff

added theorem Matrix.of_mem_specialOrthogonalGroup_fin_two_iff