A faithful formal branch remains faithful after arbitrary field extension. The construction is an embedding of the extended coordinate algebra into power series over the extension field.

theorem CCDN.isDomain_tensor_plane_quotient_of_smooth_point {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (z : Fin 2 → K) (j : Fin 2) (hz : (MvPolynomial.eval z) f = 0) (hj : (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0) : IsDomain (TensorProduct K L (MvPolynomial (Fin 2) K ⧸ Ideal.span {f}))

The coordinate algebra of an irreducible plane curve with a smooth rational point is a domain after every field extension.