Commit 2023-04-25 17:50 b7f71b0a

View on Github →

fix: add missing _root_ (#3630) Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your #align statement complains the def doesn't exist, don't change the #align; work out why it doesn't exist instead.

Estimated changes

added def Algebra.lmul
modified theorem Algebra.lmul_algebraMap
added theorem AlgHom.map_algebraMap
added def MulEquiv.ulift
added theorem mulLeft_bijective₀
added theorem mulRight_bijective₀
added theorem IsSMulRegular.pi
deleted theorem Pi.IsSMulRegular.pi
added def Unique.encodable
added theorem IsCoatom.isMaximal
added theorem IsCoatom.isProper
added theorem Covby.pred_eq
added theorem Covby.succ_eq
deleted theorem Order.Covby.pred_eq
deleted theorem Order.Covby.succ_eq
deleted theorem Order.Wcovby.le_succ
deleted theorem Order.Wcovby.pred_le
added theorem Wcovby.le_succ
added theorem Wcovby.pred_le
added theorem Finset.esymm_map_val
added theorem Finset.coe_infsep
deleted theorem Set.Finset.coe_infsep