Theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right

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_right View on Github →