English
Casting out of SignType respects composition with suitable bundled homomorphism types; any such f fixes SignType.
Русский
Выведение из SignType сохраняется под соответствующими связками гомоморфизмов и фиксирует SignType.
LaTeX
$$\forall {α β F} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType), f s = s$$
Lean4
/-- Casting out of `SignType` respects composition with suitable bundled homomorphism types. -/
theorem map_cast {α β F : Type*} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β]
[AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType) : f s = s := by apply map_cast' <;> simp
