multiplicativeClosure_eq_self — Mathlib

English

If W is multiplicative, then its multiplicative closure coincides with W.

Русский

Если W мультипликативно, то его мультипликативное замыкание равно самому W.

LaTeX

$$$W.multiplicativeClosure = W$$$

Lean4

/-- The multiplicative closure of a multiplicative property is equal to itself. -/
@[simp]
theorem multiplicativeClosure_eq_self [W.IsMultiplicative] : W.multiplicativeClosure = W :=
  by
  apply le_antisymm _ <| le_multiplicativeClosure W
  intro _ _ _ hf
  induction hf with
  | of _ hf₀ => exact hf₀
  | id x => exact W.id_mem x
  | comp_of _ _ _ hg hf => exact W.comp_mem _ _ hf hg

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