no goals
R : Type ?u.714741
S : Type ?u.714744
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
⊢ Splits φ (toPoly P) ↔ ∃ x y z, roots (map φ P) = {x, y, z}
rw [splits_iff_card_roots ha, card_eq_three]