no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.574502
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K { x // x ∈ p } = Module.rank K V
classical
  let ⟨f⟩ := quotient_prod_linearEquiv p
  exact rank_prod'.symm.trans f.rank_eq
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.574502
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
p : Submodule K V
f : ((V ⧸ p) × { x // x ∈ p }) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K { x // x ∈ p } = Module.rank K V
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.574502
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K { x // x ∈ p } = Module.rank K V
let ⟨f⟩ := quotient_prod_linearEquiv p
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.574502
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
p : Submodule K V
f : ((V ⧸ p) × { x // x ∈ p }) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K { x // x ∈ p } = Module.rank K V
exact rank_prod'.symm.trans f.rank_eq