exact — Mathlib

English

If reduce L1 = reduce L2, then mk L1 = mk L2.

Русский

Если reduce L1 = reduce L2, то mk L1 = mk L2.

LaTeX

$$$$\operatorname{reduce}(L_1) = \operatorname{reduce}(L_2) \Rightarrow \operatorname{mk}L_1 = \operatorname{mk}L_2.$$$$

Lean4

/-- If two words have a common maximal reduction, then they correspond to the same element in the
  free group. -/
@[to_additive /-- If two words have a common maximal reduction, then they correspond to the same
      element in the additive free group. -/
    ]
theorem exact (H : reduce L₁ = reduce L₂) : mk L₁ = mk L₂ :=
  Red.exact.2 ⟨reduce L₂, H ▸ reduce.red, reduce.red⟩

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