liftNCAlgHom — Mathlib

English

For v ∈ V, (equivariantOfLinearOfComm f h) v = f v.

Русский

Для любого v ∈ V выполняется (equivariantOfLinearOfComm f h) v = f v.

LaTeX

$$$ (\\mathrm{equivariantOfLinearOfComm}\\ f\\ h)\\ v = f\\ v $$$

Lean4

/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
def liftNCAlgHom (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) : A[G] →ₐ[k] B :=
  { liftNCRingHom (f : A →+* B) g h_comm with commutes' := by simp [liftNCRingHom] }

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