R : Type ?u.689546
S : Type ?u.689549
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits φ (toPoly P) ↔ ↑card (roots (map φ P)) = 3
R : Type ?u.689546
S : Type ?u.689549
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) ↔ ↑card (roots (map φ P)) = 3
replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha
R : Type ?u.689546
S : Type ?u.689549
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits (RingHom.comp (RingHom.id K) φ) (toPoly P) ↔ ↑card (roots (map φ P)) = 3
R : Type ?u.689546
S : Type ?u.689549
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits φ (toPoly P) ↔ ↑card (roots (map φ P)) = 3
nth_rw 1 [← RingHom.id_comp φ]
no goals
R : Type ?u.689546
S : Type ?u.689549
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits (RingHom.comp (RingHom.id K) φ) (toPoly P) ↔ ↑card (roots (map φ P)) = 3
rw [roots, ← splits_map_iff, ← map_toPoly, Polynomial.splits_iff_card_roots,
  ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]