LeanPool.SardMoreira.LinearAlgebra

theorem LinearMap.rank_prod_fst {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] (f : E × F →ₗ[ℝ] G) : ((fst ℝ E F).prod f).rank = Cardinal.lift.{u_3, u_1} (Module.rank ℝ E) + Cardinal.lift.{u_1, u_3} (f ∘ₗ inr ℝ E F).rank

theorem LinearMap.finrank_range_prod_fst {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (f : E × F →ₗ[ℝ] G) : Module.finrank ℝ ↥((fst ℝ E F).prod f).range = Module.finrank ℝ E + Module.finrank ℝ ↥(f ∘ₗ inr ℝ E F).range

theorem LinearMap.finrank_range_prod_fst_iff_comp_inr_eq_zero {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (f : E × F →ₗ[ℝ] G) : Module.finrank ℝ ↥((fst ℝ E F).prod f).range = Module.finrank ℝ E ↔ f ∘ₗ inr ℝ E F = 0