Theorems · Definition · group theory

AddDistribAddAction.mk.noConfusion

{M : Type u_9} →
  {N : Type u_10} →
    {inst : AddMonoid M} →
      {inst_1 : AddMonoid N} →
        {P : Sort u} →
          {toAddAction : AddAction M N} →
            {vadd_zero : ∀ (r : M), r +ᵥ 0 = 0} →
              {vadd_add : ∀ (r : M) (x y : N), r +ᵥ x + y = (r +ᵥ x) + (r +ᵥ y)} →
                {toAddAction' : AddAction M N} →
                  {vadd_zero' : ∀ (r : M), r +ᵥ 0 = 0} →
                    {vadd_add' : ∀ (r : M) (x y : N), r +ᵥ x + y = (r +ᵥ x) + (r +ᵥ y)} →
                      { toAddAction := toAddAction, vadd_zero := vadd_zero, vadd_add := vadd_add } =
                          { toAddAction := toAddAction', vadd_zero := vadd_zero', vadd_add := vadd_add' } →
                        (toAddAction ≍ toAddAction' → P) → P

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms