SubtractionMonoid.exists_zsmul_eq_of_forall_prime
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace SubtractionMonoid_exists_zsmul_eq_of_forall_primeLean source · statement
theorem _root_.SubtractionMonoid.exists_zsmul_eq_of_forall_prime {A : Type*} [SubtractionMonoid A]
(h : ∀ p : ℕ, p.Prime → ∀ x : A, ∃ y : A, (p : ℤ) • y = x) :
∀ n : ℤ, n ≠ 0 → ∀ x : A, ∃ y : A, n • y = x