Documentation

Mathlib.Algebra.Module.PUnit

Instances on PUnit #

This file collects facts about module structures on the one-element type

instance PUnit.smul {R : Type u_1} :
Equations
    instance PUnit.vadd {R : Type u_1} :
    Equations
      @[simp]
      theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1}) (r : R) :
      r y = unit
      @[simp]
      theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit.{u_4 + 1}) (r : R) :
      r +ᵥ y = unit
      Equations
        instance PUnit.module {R : Type u_1} [Semiring R] :
        Equations
          Equations
            Equations
              @[simp]
              theorem PUnit.smul_eq' {R : Type u_1} (r : PUnit.{u_3 + 1}) (a : R) :
              r a = a

              The one-element type acts trivially on every element.

              @[simp]
              theorem PUnit.vadd_eq' {R : Type u_1} (r : PUnit.{u_3 + 1}) (a : R) :
              r +ᵥ a = a