map_one — Mathlib

English

A multiplicative isomorphism sends the unit to the unit: h 1 = 1.

Русский

Мультиэквивалент сохраняет единицу: h 1 = 1.

LaTeX

$$$$ h 1 = 1. $$$$

Lean4

/-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism). -/
@[to_additive /-- An additive isomorphism of additive monoids sends `0` to `0`
      (and is hence an additive monoid isomorphism). -/
    ]
protected theorem map_one (h : M ≃* N) : h 1 = 1 :=
  map_one h

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