Theorem Algebra.finrank_eq_one_iff_bijective_algebraMap

Modification history

2026-05-07 17:04
Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
feat(NumberTheory): every number field has a ramified prime (#30666)
Added Algebra.finrank_eq_one_iff_bijective_algebraMapView on Github →