mul_def' — Mathlib

English

A definitional equality stating that the product using the irreducible multiplication matches the standard product.

Русский

Дефиниционное равенство: произведение через неприводимую операцию умножения совпадает с обычным произведением.

LaTeX

$$I.mul J = ⟨I.mul J, I.isFractional.mul J.isFractional⟩$$

Lean4

theorem mul_def' : eta_helper Eq✝ @mul.{} @(delta% @definition✝) :=
  by
  intros
  delta mul
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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