Theorem Algebra.finrank_eq_of_equiv_equiv

Modification history

2025-07-06 09:09
Mathlib/LinearAlgebra/Dimension/Finrank.lean
feat(NumberField/CMField): All CM-extensions come from the real maximal subfield (#25818) …
Added Algebra.finrank_eq_of_equiv_equivView on Github →