Multiplication by a nonzero element in a GroupWithZero is a permutation. #
@[simp]
theorem
Equiv.mulLeft₀_symm_apply
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
↑(Equiv.symm (Equiv.mulLeft₀ a ha)) = fun x => a⁻¹ * x
@[simp]
theorem
Equiv.mulLeft₀_apply
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
↑(Equiv.mulLeft₀ a ha) = fun x => a * x
Left multiplication by a nonzero element in a GroupWithZero is a permutation of the
underlying type.
Equations
- Equiv.mulLeft₀ a ha = Units.mulLeft (Units.mk0 a ha)
theorem
Equiv.mulLeft_bijective₀
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
Function.Bijective ((fun x x_1 => x * x_1) a)
@[simp]
theorem
Equiv.mulRight₀_symm_apply
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
↑(Equiv.symm (Equiv.mulRight₀ a ha)) = fun x => x * a⁻¹
@[simp]
theorem
Equiv.mulRight₀_apply
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
↑(Equiv.mulRight₀ a ha) = fun x => x * a
Right multiplication by a nonzero element in a GroupWithZero is a permutation of the
underlying type.
Equations
- Equiv.mulRight₀ a ha = Units.mulRight (Units.mk0 a ha)
theorem
Equiv.mulRight_bijective₀
{G : Type u_1}
[inst : GroupWithZero G]
(a : G)
(ha : a ≠ 0)
:
Function.Bijective fun x => x * a