Theorems · Theorem · ring theory

RingInvo.mk.sizeOf_spec

∀ {R : Type u_2} [inst : Semiring R] [inst_1 : SizeOf R] (toRingEquiv : R ≃+* Rᵐᵒᵖ)
  (involution' : ∀ (x : R), MulOpposite.unop (toRingEquiv.toFun (MulOpposite.unop (toRingEquiv.toFun x))) = x),
  sizeOf { toRingEquiv := toRingEquiv, involution' := involution' } = 1 + sizeOf toRingEquiv

Defined in: Mathlib.RingTheory.RingInvo
Cited by: 0 results in Mathlib
Foundations: Depth 17 from the axioms · uses no axioms
Assumes: Semiring SizeOf

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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

Semiringstatement and proof · cited by 13,802
RingEquivstatement and proof · cited by 1,147
MulOppositestatement and proof · cited by 1,135
Equiv.toFunstatement and proof · cited by 279
MulOpposite.unopstatement and proof · cited by 268
RingEquiv.toEquivstatement and proof · cited by 101
RingInvostatement · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.