mathlib documentation


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) :

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

theorem is_unit.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : is_unit x) :
theorem squarefree_one {R : Type u_1} [comm_monoid R] :
theorem not_squarefree_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] :
theorem irreducible.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : irreducible x) :
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) :
theorem nat.sum_divisors_filter_squarefree {n : } (h0 : n 0) {α : Type u_1} [add_comm_monoid α] {f : → α} :