English
There exists a copy operation that produces a new unit with the same structure as the original, using new data but preserving the unit properties.
Русский
Существует операция копирования, создающая новую единицу с той же структурой, используя новые данные, но сохраняющую свойства единицы.
LaTeX
$$$$ \\text{copy}(u, v, hv, w, hw) \\in \\alpha^{\\times}. $$$$
Lean4
/-- Copy a unit, adjusting definition equalities. -/
@[to_additive (attr := simps) /-- Copy an `AddUnit`, adjusting definitional equalities. -/
]
def copy (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑u⁻¹) : αˣ :=
{ val, inv, inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }
