Mathlib Map

Theorems · Theorem · group theory

Rep.finsupp_V

∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (α : Type u') (A : Rep.{u_1, u, v} k G),
  ↑(Rep.finsupp α A) = (α →₀ ↑A)
Defined in
Mathlib.RepresentationTheory.Rep.Basic
Cited by
0 results in Mathlib
Foundations
Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CommRing · cited by 17173CommRingFinsupp · cited by 5255FinsuppMonoid · cited by 3887MonoidRep · cited by 843RepRep.V · cited by 695Rep.VRep.finsupp · cited by 1Rep.finsuppRep.finsupp_VCITED BYCITES

Cites6

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

  • CommRingstatement and proof · cited by 17,173
  • Finsuppstatement · cited by 5,255
  • Monoidstatement and proof · cited by 3,887
  • Repstatement and proof · cited by 843
  • Rep.Vstatement · cited by 695
  • Rep.finsuppstatement · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.