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.
theorem
SemiconjBy.zpow_right₀
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{x : G₀}
{y : G₀}
(h : SemiconjBy a x y)
(m : ℤ)
:
SemiconjBy a (x ^ m) (y ^ m)
theorem
Commute.zpow_right₀
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : Commute a b)
(m : ℤ)
:
theorem
Commute.zpow_left₀
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : Commute a b)
(m : ℤ)
:
theorem
Commute.zpow_zpow_self₀
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
(a : G₀)
(m : ℤ)
(n : ℤ)
:
theorem
zpow_ne_zero_of_ne_zero
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
(ha : a ≠ 0)
(z : ℤ)
:
theorem
zpow_eq_zero
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{x : G₀}
{n : ℤ}
(h : x ^ n = 0)
:
x = 0
@[simp]
theorem
map_zpow₀
{F : Type u_1}
{G₀ : Type u_2}
{G₀' : Type u_3}
[inst : GroupWithZero G₀]
[inst : GroupWithZero G₀']
[inst : MonoidWithZeroHomClass F G₀ G₀']
(f : F)
(x : G₀)
(n : ℤ)
:
If a monoid homomorphism f
between two GroupWithZero
s maps 0
to 0
, then it maps x^n
,
n : ℤ
, to (f x)^n
.