Theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left

Modification history

2024-11-28 16:12
Mathlib/LinearAlgebra/Matrix/BaseChange.lean
feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField` (#18940)
Added Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_leftView on Github →