Theorem Matrix.mul_eq_one_comm_of_card_eq

Modification history

2025-12-28 17:51
Mathlib/Data/Matrix/Mul.lean
feat(Algebra): stably finite rings (#32262) …
Added Matrix.mul_eq_one_comm_of_card_eqView on Github →