Theorems · Theorem · commutative algebra

LinearEquiv.piUnique_apply

∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)],
  ⇑(LinearEquiv.piUnique R f) = (Equiv.piUnique f).toFun

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

0 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

UniqueSemiringAddCommMonoidModule