multiplicativeClosure_eq_self_iff

English

The multiplicative closure equals the original property if and only if the property is multiplicative.

Русский

Замыкание по умножению равно исходному свойству тогда и только тогда, когда свойство мультипликативно.

LaTeX

$$$W.multiplicativeClosure = W \iff W.IsMultiplicative$$$

Lean4

theorem multiplicativeClosure_eq_self_iff : W.multiplicativeClosure = W ↔ W.IsMultiplicative
    where
  mp
    h := by
    rw [← h]
    infer_instance
  mpr h := multiplicativeClosure_eq_self W

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