ratCast

Mathlib.Algebra.Field.TransferInstance

URI: https://scilib.ai/kg/mathlib#Equiv.ratCast

English

Given an equivalence e: α ≃ β, transfer an NNRatCast from β to α by composing with e^{-1}.

Русский

Для эквивалентности e: α ≃ β переносим NNRatCast с β на α по композиции с её обратной.

LaTeX

$$$\text{nnratCast } q := e^{-1}(q)$$$

Lean4

/-- Transfer `RatCast` across an `Equiv` -/
protected abbrev ratCast [RatCast β] : RatCast α where ratCast n := e.symm n

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

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

Разделы

Аффилиация

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