Theorems · Theorem · nonassociative algebras

LieRinehartAlgebra.Hom.mk.sizeOf_spec

∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : CommRing A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {σ : A₁ →ₐ[R] A₂} {L₁ : Type u_8} {L₂ : Type u_9}
  [inst_5 : LieRing L₁] [inst_6 : Module A₁ L₁] [inst_7 : LieRingModule L₁ A₁] [inst_8 : LieAlgebra R L₁]
  [inst_9 : LieRing L₂] [inst_10 : Module A₂ L₂] [inst_11 : LieRingModule L₂ A₂] [inst_12 : LieAlgebra R L₂]
  [inst_13 : SizeOf R] [inst_14 : SizeOf A₁] [inst_15 : SizeOf A₂] [inst_16 : SizeOf L₁] [inst_17 : SizeOf L₂]
  (toLieHom : L₁ →ₗ⁅R⁆ L₂) (map_smul_apply' : ∀ (a : A₁) (x : L₁), toLieHom (a • x) = σ a • toLieHom x)
  (apply_lie' : ∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom x, σ a⁆),
  sizeOf { toLieHom := toLieHom, map_smul_apply' := map_smul_apply', apply_lie' := apply_lie' } = 1 + sizeOf toLieHom

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

CommRingCommRingCommRingAlgebraAlgebraLieRingModuleLieRingModuleLieAlgebraLieRingModuleLieRingModuleLieAlgebraSizeOfSizeOfSizeOfSizeOfSizeOf