Commit 2025-04-19 07:34 2d6e7438

View on Github →

chore(*): rename Prod.map lemmas (#24189) Also rename some Prod.fst and Prod.snd lemmas and add 2 dot notation lemmas.

Estimated changes

deleted theorem MDifferentiable.prod_map
deleted theorem tangentMapWithin_prod_fst
deleted theorem tangentMapWithin_prod_snd
added theorem tangentMap_prodFst
added theorem tangentMap_prodSnd
deleted theorem tangentMap_prod_fst
deleted theorem tangentMap_prod_snd
added theorem Antitone.prodMap
deleted theorem Antitone.prod_map
added theorem Monotone.prodMap
deleted theorem Monotone.prod_map
added theorem StrictAnti.prodMap
deleted theorem StrictAnti.prod_map
added theorem StrictMono.prodMap
deleted theorem StrictMono.prod_map
added theorem Isometry.prodMap
deleted theorem Isometry.prod_map