Commit 2024-01-07 19:34 9f6d3388

View on Github →

chore(*): replace $ with <| (#9319) See Zulip thread for the discussion.

Estimated changes

modified def Cache.IO.mkBuildPaths
modified theorem MulOpposite.op_inj
modified theorem sub_one_lt
modified theorem right_ne_zero_of_smul
modified theorem Int.card_Icc
modified theorem Int.card_Ico
modified theorem Int.card_Ioc
modified theorem Int.card_Ioo
modified theorem Nat.ModEq.of_dvd
modified theorem Nat.modEq_one
modified theorem Nat.modEq_sub
modified theorem Set.projIci_of_le
modified theorem Set.projIic_of_le
modified theorem Set.uIcc_of_not_ge
modified theorem Set.uIcc_of_not_le
modified theorem pow_injOn_Iio_orderOf
modified theorem Subgroup.closure_eq_bot_iff
modified theorem Submonoid.powers_one
modified theorem LinearMap.disjoint_inl_inr
modified theorem LinearMap.sup_range_inl_inr
modified theorem Filter.ker_eq_univ
modified theorem Sublattice.map_id
modified def CountNested.nested1