tacticHopf_tensor_induction_With__

English

For x ∈ A and y ∈ B, the counit on x ⊗ y in the tensor product equals the corresponding product under the base scalars: counit on tensor equals the product of counits on the factors.

Русский

Для x ∈ A и y ∈ B, counit на x ⊗ y в тензорном произведении равен произведению counit на факторах.

LaTeX

$$$\operatorname{counit}_R^{A\otimes B}(x \otimes y) = \operatorname{counit}_R^A(x) \cdot \operatorname{counit}_R^B(y).$$$

Lean4

/-- `hopf_tensor_induction x with x₁ x₂` attempts to replace `x` by
`x₁ ⊗ₜ x₂` via linearity. This is an implementation detail that is used to set up tensor products
of coalgebras, bialgebras, and hopf algebras, and shouldn't be relied on downstream. -/
@[scoped tactic_parser 1000]
public meta def tacticHopf_tensor_induction_With__ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `TensorProduct.tacticHopf_tensor_induction_With__ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "hopf_tensor_induction " false✝)
            Lean.Parser.Tactic.elimTarget)
          (ParserDescr.symbol✝ "with "))
        (ParserDescr.const✝ `ident))
      (ParserDescr.const✝ `ident))

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