finite_right

Mathlib.Data.Finite.Prod

URI: https://scilib.ai/kg/mathlib#MulEquiv.finite_right

English

If β is finite, then the group of multiplicative equivalences α ≃* β is finite.

Русский

Если β конечно, то множество мультиэквивалентов α ≃* β конечно.

LaTeX

$$$ \\text{Finite}(\\beta) \\Rightarrow \\text{Finite}(\\alpha \\simeq^* \\beta) $$$

Lean4

@[to_additive]
instance finite_right {α β : Type*} [Mul α] [Mul β] [Finite β] : Finite (α ≃* β) :=
  Finite.of_injective toEquiv toEquiv_injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru