mk_tmul_inv — Mathlib

English

Similarly, in the coinvariants, the element x ⊗ (τ(g)⁻¹ y) is identified with (ρ(g) x) ⊗ y.

Русский

Аналогично: в когонвариантах x ⊗ (τ(g)⁻¹ y) идентифицируется с (ρ(g) x) ⊗ y.

LaTeX

$$mk_tmul_inv : Coinvariants (ρ.tprod τ) (x ⊗ τ(g)^{-1} y) = Coinvariants (ρ.tprod τ) (ρ(g) x ⊗ y)$$

Lean4

@[simp]
theorem mk_tmul_inv (x : V) (y : W) (g : G) :
    Coinvariants.mk (ρ.tprod τ) (x ⊗ₜ[k] τ g⁻¹ y) = Coinvariants.mk (ρ.tprod τ) (ρ g x ⊗ₜ[k] y) :=
  (mk_eq_iff _).2 <| mem_ker_of_eq g⁻¹ (ρ g x ⊗ₜ[k] y) _ <| by simp

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