Irreducible.squarefree
theorem Irreducible.squarefree : ∀ {R : Type u_1} [inst : CommMonoid R] {x : R}, Irreducible x → Squarefree x := by
sorry
This theorem states that for any type `R` that forms a commutative monoid, and any element `x` of `R`, if `x` is irreducible then it is squarefree. In terms of mathematics, for a given irreducible element in a commutative monoid, the only squares that divide it are the squares of units. In other words, the element is squarefree if it cannot be divided by the square of any non-unit element.
More concisely: For any commutative monoid `R` and irreducible element `x` in `R`, `x` is squarefree, i.e., the only squares dividing `x` are those of units in `R`.
|
Squarefree.squarefree_of_dvd
theorem Squarefree.squarefree_of_dvd :
∀ {R : Type u_1} [inst : CommMonoid R] {x y : R}, x ∣ y → Squarefree y → Squarefree x
The theorem states that for any given commutative monoid `R` and any two elements `x` and `y` of `R`, if `x` divides `y` and `y` is squarefree (meaning the only squares that divide it are the squares of units), then `x` is also squarefree. In mathematical terms, if $x | y$ and $y$ is squarefree, then $x$ is squarefree as well.
More concisely: If a commutative monoid element `x` divides a squarefree element `y`, then `x` is also squarefree.
|
Squarefree.isRadical
theorem Squarefree.isRadical :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : DecompositionMonoid R] {x : R},
Squarefree x → IsRadical x
The theorem `Squarefree.isRadical` states that for any commutative monoid with zero `R` with the structure of a decomposition monoid, every squarefree element `x` in `R` is also radical. In other words, if an element `x` in `R` is such that the only squares that divide it are the squares of units, then `x` also has the property that it divides any element `y` if it divides a power of `y`.
More concisely: In a commutative monoid with zero endowed with a decomposition structure, every squarefree element is radical.
|
multiplicity.squarefree_iff_multiplicity_le_one
theorem multiplicity.squarefree_iff_multiplicity_le_one :
∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : DecidableRel Dvd.dvd] (r : R),
Squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ IsUnit x
The theorem `multiplicity.squarefree_iff_multiplicity_le_one` states that for any commutative monoid `R` with a decidable relation of divisibility `Dvd.dvd`, an element `r` of `R` is square-free (meaning the only squares that divide it are the squares of units) if and only if for all elements `x` of `R`, the multiplicity of `x` in `r` (the largest natural number `n` such that `x^n` divides `r`) is less than or equal to one, or `x` is a unit (an element with a two-sided inverse). In other words, an element is square-free if each of its divisors appears at most once in the factorization, unless the divisor is a unit.
More concisely: An element in a commutative monoid is square-free if and only if the multiplicity of each non-unit divisor is at most 1.
|
Squarefree.ne_zero
theorem Squarefree.ne_zero :
∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : Nontrivial R] {m : R}, Squarefree m → m ≠ 0
The theorem `Squarefree.ne_zero` states that for any type `R` which has instances of `MonoidWithZero` and `Nontrivial` (i.e. it is a monoid with a distinguished zero element and there exists at least one element that is not equal to zero), and any element `m` of `R`, if `m` is squarefree (which means that the only squares that can divide it are the squares of unit elements), then `m` cannot be equal to zero.
More concisely: If `m` is a squarefree element in a monoid `R` with zero and at least one non-zero element, then `m` is distinct from zero.
|