SubtractionMonoid.exists_zsmul_eq_of_forall_prime_nsmul
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_prime_nsmulLean source · statement
theorem _root_.SubtractionMonoid.exists_zsmul_eq_of_forall_prime_nsmul {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