Theorem: FiniteDimensional.finrank_quotient (FltRegular/NumberTheory/Finrank.lean)

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
⊢ finrank R (M ⧸ N) = finrank R M - finrank R ↥N
Tactic:
rw [← FiniteDimensional.finrank_add_finrank_quotient N, add_tsub_cancel_left]
State after:
no goals