Commit 2023-10-16 09:02 38db8256

View on Github →

chore(RingTheory/PowerSeries/Basic): remove open Classical (#7665) Only two lemma statements have changed:

  • coeff_truncFun now contains the missing [DecidableEq σ] needed to make the statement make sense
  • order_eq_multiplicity_X now contains a missing DecidableRel argument needed to make the RHS fully general. Everywhere else, classical has just been inserted into the proof.

Estimated changes