mathlib documentation

algebra.squarefree

Squarefree elements of monoids #

An element of a monoid is squarefree when it is not divisible by any squares except the squares of units.

Main Definitions #

Main Results #

Tags #

squarefree, multiplicity

def squarefree {R : Type u_1} [monoid R] (r : R) :
Prop

An element of a monoid is squarefree if the only squares that divide it are the squares of units.

Equations
@[simp]
theorem is_unit.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : is_unit x) :
@[simp]
theorem squarefree_one {R : Type u_1} [comm_monoid R] :
@[simp]
theorem not_squarefree_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] :
@[simp]
theorem irreducible.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : irreducible x) :
@[simp]
theorem prime.squarefree {R : Type u_1} [comm_cancel_monoid_with_zero R] {x : R} (h : prime x) :
theorem squarefree_of_dvd_of_squarefree {R : Type u_1} [comm_monoid R] {x y : R} (hdvd : x y) (hsq : squarefree y) :
@[protected, instance]
Equations
theorem nat.sum_divisors_filter_squarefree {n : } (h0 : n 0) {α : Type u_1} [add_comm_monoid α] {f : → α} :
theorem nat.sq_mul_squarefree_of_pos {n : } (hn : 0 < n) :
∃ (a b : ), 0 < a 0 < b (b ^ 2) * a = n squarefree a
theorem nat.sq_mul_squarefree_of_pos' {n : } (h : 0 < n) :
∃ (a b : ), ((b + 1) ^ 2) * (a + 1) = n squarefree (a + 1)
theorem nat.sq_mul_squarefree (n : ) :
∃ (a b : ), (b ^ 2) * a = n squarefree a