Documentation

Mathlib.Algebra.PUnitInstances.Module

Instances on PUnit #

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

instance PUnit.vadd {R : Type u_1} :
Equations
instance PUnit.smul {R : Type u_1} :
Equations
@[simp]
theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
@[simp]
theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] :
Equations
  • =
Equations
Equations
Equations
Equations
Equations
Equations
instance PUnit.module {R : Type u_1} [Semiring R] :
Equations