Theorems · Theorem · ring theory

Unitization.fstHom_apply

∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : Unitization R A),
  (Unitization.fstHom R A) a = a.toProd.1

Defined in

Mathlib.Algebra.Algebra.Unitization

Cited by

2 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringNonUnitalSemiringModuleIsScalarTowerSMulCommClass