theorem
L26 ↗ord_smul_of_ne_zero
AlgebraicCurve.Place.ord_smul_of_ne_zero
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_smul_of_ne_zero
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.ord_smul_of_ne_zero {K F : Type*} [Field K] [Field F] [Algebra
K F] (v : Place K F) {c : K} (hc : c ≠ 0) (x : F) : v.ord (c • x) = v.ord x