R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card ((M ⧸ S) × { x // x ∈ S })
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card { x // x ∈ S } * Fintype.card (M ⧸ S)
rw [mul_comm, ← Fintype.card_prod]
no goals
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card ((M ⧸ S) × { x // x ∈ S })
exact Fintype.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup