Theorems · Theorem · ring theory

Coalgebra.TensorProduct.lid_symm_apply

∀ {R : Type u_5} {P : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid P] [inst_2 : Module R P]
  [inst_3 : Coalgebra R P] (a : P), (Coalgebra.TensorProduct.lid R P).symm a = 1 ⊗ₜ[R] a

Defined in

Mathlib.RingTheory.Coalgebra.TensorProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebra