Theorem Real.rank_rat_real

Modification history

2024-06-13 02:15

Mathlib/Data/Complex/FiniteDimensional.lean

chore: split Mathlib.Data.Complex.Module (#13762)

Modified Real.rank_rat_real View on Github →

2023-08-22 03:35

Mathlib/Data/Complex/Module.lean

feat: compute rank of `ℂ` and `ℝ` as `ℚ`-modules (#6672) …

Added Real.rank_rat_real View on Github →