Commit 2024-03-13 20:53 59f72a90

View on Github →

chore: remove more autoImplicit (#11336) ... or reduce its scope (the full removal is not as obvious).

Estimated changes

modified theorem GroupCat.forget_map
modified theorem GroupWithZeroCat.forget_map
modified theorem MonCat.forget_map
modified theorem CommRingCat.forget_map
modified theorem CommSemiRingCat.forget_map
modified theorem RingCat.forget_map
modified theorem SemiRingCat.forget_map
modified theorem CauSeq.smul_equiv_smul
modified theorem PUnit.div_eq
modified theorem PUnit.gcd_eq
modified theorem PUnit.inv_eq
modified theorem PUnit.lcm_eq
modified theorem PUnit.mul_eq
modified theorem pred_ne_self
modified theorem succ_ne_self
modified theorem SSet.Truncated.hom_ext
modified theorem NFA.mem_accepts
modified theorem Finset.inf'_le_of_le
modified theorem Int.cast_Nat_cast
modified theorem Int.cast_id
modified theorem Int.cast_mul
modified theorem Int.cast_pow