Commit 2025-03-11 02:02 cc171ac5

View on Github →

chore(Data/S*): process a batch of porting notes (#22765)

Estimated changes

Modified Mathlib/Data/Semiquot.lean

Modified Mathlib/Data/Seq/Computation.lean

added theorem Computation.mem_pure_iff

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Seq/Seq.lean

Modified Mathlib/Data/Seq/WSeq.lean

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/Data/Set/Insert.lean

Modified Mathlib/Data/Set/Pairwise/Lattice.lean

Modified Mathlib/Data/Set/Subsingleton.lean

Modified Mathlib/Data/SetLike/Basic.lean

Modified Mathlib/Data/Sigma/Order.lean

Modified Mathlib/Data/Sign.lean

modified theorem SignType.lt_one_iff

modified theorem SignType.neg_eq_self_iff

modified theorem SignType.neg_iff

modified theorem SignType.neg_one_lt_iff

modified theorem SignType.nonneg_iff

modified theorem SignType.nonneg_iff_ne_neg_one

modified theorem SignType.nonpos_iff

modified theorem SignType.nonpos_iff_ne_one

modified theorem SignType.pos_iff

modified theorem SignType.self_eq_neg_iff

modified theorem exists_signed_sum'

modified theorem exists_signed_sum

Modified Mathlib/Data/Stream/Defs.lean

Modified Mathlib/Data/Stream/Init.lean

Modified Mathlib/Data/Subtype.lean

modified theorem Subtype.mk_eq_mk