Theorems · Theorem · ring theory

GroupLike.mk.sizeOf_spec

∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [inst_4 : SizeOf R] [inst_5 : SizeOf A] (val : A)
  (isGroupLikeElem_val : IsGroupLikeElem R val),
  sizeOf { val := val, isGroupLikeElem_val := isGroupLikeElem_val } = 1 + sizeOf val + sizeOf isGroupLikeElem_val

Defined in: Mathlib.RingTheory.Coalgebra.GroupLike
Cited by: 0 results in Mathlib
Foundations: Depth 10 from the axioms · uses no axioms
Assumes: CommSemiring AddCommMonoid Module Coalgebra SizeOf SizeOf

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Coalgebrastatement and proof · cited by 112
IsGroupLikeElemstatement and proof · cited by 39
GroupLikestatement · cited by 19

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.