Powers of elements of groups with an adjoined zero element
In this file we define integer power functions for groups with an adjoined zero element. This generalises the integer power function on a division ring.
@[simp]
@[instance]
Equations
- int.has_pow = {pow := fpow _inst_1}
@[simp]
theorem
fpow_of_nat
{G₀ : Type u_1}
[group_with_zero G₀]
(a : G₀)
(n : ℕ) :
a ^ int.of_nat n = a ^ n
theorem
semiconj_by.fpow_right
{G₀ : Type u_1}
[group_with_zero G₀]
{a x y : G₀}
(h : semiconj_by a x y)
(m : ℤ) :
semiconj_by a (x ^ m) (y ^ m)
theorem
commute.fpow_right
{G₀ : Type u_1}
[group_with_zero G₀]
{a b : G₀}
(h : commute a b)
(m : ℤ) :
theorem
commute.fpow_left
{G₀ : Type u_1}
[group_with_zero G₀]
{a b : G₀}
(h : commute a b)
(m : ℤ) :
theorem
commute.fpow_fpow
{G₀ : Type u_1}
[group_with_zero G₀]
{a b : G₀}
(h : commute a b)
(m n : ℤ) :
@[simp]
theorem
fpow_ne_zero_of_ne_zero
{G₀ : Type u_1}
[group_with_zero G₀]
{a : G₀}
(ha : a ≠ 0)
(z : ℤ) :
theorem
monoid_with_zero_hom.map_fpow
{G₀ : Type u_1}
{G₀' : Type u_2}
[group_with_zero G₀]
[group_with_zero G₀']
(f : monoid_with_zero_hom G₀ G₀')
(x : G₀)
(n : ℤ) :
If a monoid homomorphism f
between two group_with_zero
s maps 0
to 0
, then it maps x^n
,
n : ℤ
, to (f x)^n
.