mathlib documentation


Squarefree elements of monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. An element of a monoid is squarefree when it is not divisible by any squares except the squares of units.

Results about squarefree natural numbers are proved in data/nat/squarefree.

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.

Instances for squarefree
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 squarefree.ne_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] {m : R} (hm : squarefree m) :
m 0
theorem irreducible.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : irreducible x) :
theorem prime.squarefree {R : Type u_1} [cancel_comm_monoid_with_zero R] {x : R} (h : prime x) :
theorem squarefree.of_mul_left {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :
theorem squarefree.of_mul_right {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :
theorem squarefree.squarefree_of_dvd {R : Type u_1} [comm_monoid R] {x y : R} (hdvd : x y) (hsq : squarefree y) :
theorem squarefree.gcd_right {α : Type u_2} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) {b : α} (hb : squarefree b) :
theorem squarefree.gcd_left {α : Type u_2} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a : α} (b : α) (ha : squarefree a) :
theorem multiplicity.finite_prime_left {R : Type u_1} [cancel_comm_monoid_with_zero R] [wf_dvd_monoid R] {a b : R} (ha : prime a) (hb : b 0) :
theorem is_radical.squarefree {R : Type u_1} [cancel_comm_monoid_with_zero R] {x : R} (h0 : x 0) (h : is_radical x) :