Further lemmas about units in a MonoidWithZero
or a GroupWithZero
. #
@[simp]
@[simp]
theorem
div_eq_of_eq_mul
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
{c : G₀}
(hb : b ≠ 0)
:
theorem
eq_div_of_mul_eq
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
{c : G₀}
(hc : c ≠ 0)
:
theorem
div_eq_one_iff_eq
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
(hb : b ≠ 0)
:
theorem
div_mul_cancel_of_imp
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : b = 0 → a = 0)
:
theorem
mul_div_cancel_of_imp
{G₀ : Type u_1}
[inst : GroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : b = 0 → a = 0)
:
theorem
div_mul_right
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
(b : G₀)
(ha : a ≠ 0)
:
theorem
mul_div_cancel_left_of_imp
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : a = 0 → b = 0)
:
theorem
mul_div_cancel_left
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
(b : G₀)
(ha : a ≠ 0)
:
theorem
mul_div_cancel_of_imp'
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
{b : G₀}
(h : b = 0 → a = 0)
:
theorem
mul_div_cancel'
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{b : G₀}
(a : G₀)
(hb : b ≠ 0)
:
theorem
div_div_cancel'
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
{b : G₀}
(ha : a ≠ 0)
:
theorem
div_div_cancel_left'
{G₀ : Type u_1}
[inst : CommGroupWithZero G₀]
{a : G₀}
{b : G₀}
(ha : a ≠ 0)
:
theorem
map_ne_zero
{M₀ : Type u_1}
{G₀ : Type u_3}
{F : Type u_2}
[inst : MonoidWithZero M₀]
[inst : GroupWithZero G₀]
[inst : Nontrivial M₀]
[inst : MonoidWithZeroHomClass F G₀ M₀]
(f : F)
{a : G₀}
:
@[simp]
theorem
map_eq_zero
{M₀ : Type u_1}
{G₀ : Type u_3}
{F : Type u_2}
[inst : MonoidWithZero M₀]
[inst : GroupWithZero G₀]
[inst : Nontrivial M₀]
[inst : MonoidWithZeroHomClass F G₀ M₀]
(f : F)
{a : G₀}
:
theorem
eq_on_inv₀
{G₀ : Type u_3}
{M₀' : Type u_1}
{F' : Type u_2}
[inst : GroupWithZero G₀]
[inst : MonoidWithZero M₀']
[inst : MonoidWithZeroHomClass F' G₀ M₀']
{a : G₀}
(f : F')
(g : F')
(h : ↑f a = ↑g a)
:
@[simp]
theorem
map_inv₀
{G₀ : Type u_2}
{G₀' : Type u_1}
{F : Type u_3}
[inst : GroupWithZero G₀]
[inst : GroupWithZero G₀']
[inst : MonoidWithZeroHomClass F G₀ G₀']
(f : F)
(a : G₀)
:
A monoid homomorphism between groups with zeros sending 0
to 0
sends a⁻¹⁻¹
to (f a)⁻¹⁻¹
.
@[simp]
theorem
map_div₀
{G₀ : Type u_2}
{G₀' : Type u_1}
{F : Type u_3}
[inst : GroupWithZero G₀]
[inst : GroupWithZero G₀']
[inst : MonoidWithZeroHomClass F G₀ G₀']
(f : F)
(a : G₀)
(b : G₀)
:
We define the inverse as a MonoidWithZeroHom
by extending the inverse map by zero
on non-units.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
MonoidWithZero.coe_inverse
{M : Type u_1}
[inst : CommMonoidWithZero M]
:
↑MonoidWithZero.inverse = Ring.inverse
@[simp]
theorem
MonoidWithZero.inverse_apply
{M : Type u_1}
[inst : CommMonoidWithZero M]
(a : M)
:
↑MonoidWithZero.inverse a = Ring.inverse a
Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.
Equations
- One or more equations did not get rendered due to their size.