Commit 2024-02-27 06:49 c19d45ab

View on Github →

feat(Data/Sign): some more API for SignType (#10920) Since Real.sign etc are being deprecated in favour of the generic SignType.sign, this PR adds some more API for the latter: in particular, compatibility of the canonical maps in and out of SignType with maps satisfying suitable assumptions. This is a prerequisite for #10011.

Estimated changes

Modified Mathlib/Data/Sign.lean

added theorem SignType.coe_neg

added theorem SignType.map_cast'

added theorem SignType.map_cast

added theorem StrictMono.sign_comp