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

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 : → α} :