Theorems · Theorem · group theory

MonoidWithZeroHom.valueGroup.mk_mul

∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {r₁ s₁ r₂ s₂ : A}
  {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0},
  MonoidWithZeroHom.valueGroup.mk f r₁ s₁ hr₁ hs₁ * MonoidWithZeroHom.valueGroup.mk f r₂ s₂ hr₂ hs₂ =
    MonoidWithZeroHom.valueGroup.mk f (r₁ * r₂) (s₁ * s₂) ⋯ ⋯

Defined in

Mathlib.Algebra.GroupWithZero.Range

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidWithZeroCommGroupWithZero