lift_mk — Mathlib

English

The map between coinvariants induced by a linear map f satisfies map ρ τ f hf (mk ρ x) = mk τ (f x).

Русский

Отображение между коинвариантами, индуцированное линейным отображением f, удовлетворяет map ρ τ f hf (mk ρ x) = mk τ (f x).

LaTeX

$$$\mathrm{map}\_{\rho,\tau} f\, hf (mk_\rho x) = mk_\tau (f x)$$$

Lean4

@[simp]
theorem lift_mk (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) (x : V) : lift ρ f h (mk _ x) = f x :=
  rfl

Похожие утверждения