Commit 2024-09-16 12:43 1b1a0918

View on Github →

refactor(Mathlib/CategoryTheory/Monoidal/Transport): remove simps at transport (#16819) We get better simp normal forms not by unfolding transport but instead putting simps! at the definition that uses transport. The compiling time is also improved.

Estimated changes

deleted theorem Action.associator_hom_hom
deleted theorem Action.associator_inv_hom
deleted theorem Action.leftUnitor_hom_hom
deleted theorem Action.leftUnitor_inv_hom
deleted theorem Action.tensorUnit_rho
deleted theorem Action.tensorUnit_v
added theorem Action.tensorUnit_ρ'
added theorem Action.tensorUnit_ρ
deleted theorem Action.tensor_hom
deleted theorem Action.tensor_rho
deleted theorem Action.tensor_v
added theorem Action.tensor_ρ'
added theorem Action.tensor_ρ
deleted theorem Action.whiskerLeft_hom
deleted theorem Action.whiskerRight_hom
deleted theorem FDRep.char_tensor'