Theorems · Theorem · linear algebra
Complex.finrank_real_complex
Module.finrank ℝ ℂ = 2
ℂ is a finite extension of ℝ of degree 2, i.e [ℂ : ℝ] = 2
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement · cited by 5,565
- Module.finrankstatement · cited by 1,770
- Fintype.card_finproof · cited by 270
- Module.finrank_eq_card_basisproof · cited by 40
- Complex.basisOneIproof · cited by 16
Cited by11
Results whose statement or proof uses this declaration.
- Complex.finrank_real_complex_factproof · cited by 6
- Complex.rank_real_complexproof · cited by 4
- NumberField.mixedEmbedding.finrankproof · cited by 4
- NumberField.InfinitePlace.IsRamified.finrank_eq_twoproof · cited by 3
- Complex.volume_ballproof · cited by 3
- Irreducible.natDegree_le_twoproof · cited by 2
- Complex.volume_sum_rpow_ltproof · cited by 1
- Complex.volume_sum_rpow_lt_oneproof · cited by 1
- Complex.rank_real_complex'proof · cited by 1
- Real.nonempty_algEquiv_orproof · cited by 1
- finrank_real_of_complexproof · cited by 0