Documentation

Monlib.LinearAlgebra.Coalgebra.MulOpposite

@[simp]
theorem LinearMap.op_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] (f : A →ₗ[R] B) :
noncomputable instance MulOpposite.coalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] :
Equations