Complex number as a finite dimensional vector space over ℝ

This file contains the FiniteDimensional ℝ ℂ instance, as well as some results about the rank (finrank and Module.rank).

instance Complex.instFiniteDimensionalReal : FiniteDimensional ℝ ℂ

@[simp]

theorem Complex.finrank_real_complex : Module.finrank ℝ ℂ = 2

ℂ is a finite extension of ℝ of degree 2, i.e [ℂ : ℝ] = 2

Stacks Tag 09G4

@[simp]

theorem Complex.rank_real_complex : Module.rank ℝ ℂ = 2

theorem Complex.rank_real_complex' : Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

theorem Complex.finrank_real_complex_fact : Fact (Module.finrank ℝ ℂ = 2)

Fact version of the dimension of ℂ over ℝ, locally useful in the definition of the circle.

@[instance 100]

instance FiniteDimensional.complexToReal (E : Type u_1) [AddCommGroup E] [Module ℂ E] [FiniteDimensional ℂ E] : FiniteDimensional ℝ E

theorem rank_real_of_complex (E : Type u_1) [AddCommGroup E] [Module ℂ E] : Module.rank ℝ E = 2 * Module.rank ℂ E

theorem finrank_real_of_complex (E : Type u_1) [AddCommGroup E] [Module ℂ E] : Module.finrank ℝ E = 2 * Module.finrank ℂ E

@[simp]

theorem Real.rank_rat_real : Module.rank ℚ ℝ = Cardinal.continuum

@[simp]

theorem Complex.rank_rat_complex : Module.rank ℚ ℂ = Cardinal.continuum

C has an uncountable basis over ℚ.

Stacks Tag 09G0

theorem Complex.nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ)

ℂ and ℝ are isomorphic as vector spaces over ℚ, or equivalently, as additive groups.