The image of prime multiplication is Zariski constructible
ProvedPhilipponMultiplicity.prime_nsmul_range_is_constructibleLet be a commutative algebraic group over a Philippon base field , and let be a prime integer. In the Zariski topology on the actual group points, the image of multiplication by is constructible:
Thus the image belongs to the Boolean algebra generated by Zariski-open subsets. This is the constructibility input for converting a local dominance statement into a nonempty open set of divisible points. Connectedness is not assumed, and zero-dimensional groups are included.
Formalization Note. The proof establishes regularity of integer multiplication from the actual embedded-group regularity hypotheses and applies constructibility of regular-map images. The constructibility theorem and its affine chart dependencies are now proved, completing the prime-multiplication image statement. Every theorem dependency of the accepted reduction is now Proved, and this theorem has zero Open leaves. The final affine construction is proved here. The original formal statement and hypotheses are unchanged.
import Mathlib.Topology.Constructible import Definitions.Def_PhilipponMultiplicity_Geometry set_option autoImplicit false
namespace PhilipponMultiplicity
theorem prime_nsmul_range_is_constructible
(K : Type*) [NontriviallyNormedField K] (hK : IsPhilipponBaseField K)
(G : EmbeddedGroupProduct K) (p : ℕ) (hp : p.Prime) :
@Topology.IsConstructible G.Point G.zariskiTopology (Set.range (fun x : G.Point => p • x)) := by sorry
end PhilipponMultiplicity