Theorem LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo

Modification history

2023-12-12 11:45
Mathlib/LinearAlgebra/FiniteSpan.lean
feat: definition of reflections and root system uniqueness lemma (#8981)
Added LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsToView on Github →