Miyahara Kō

Display of unit.star is glitched

1

As this screenshot, display of `unit.star` is glitched.  OS is android. Here is the link. [matrix.pivot.list_transvec_col_mul_last_row_drop](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/transvection.html#matrix.pivot.list_transvec_col_mul_last_row_drop)

feat: port `cc` tactic (3/3)

3

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/cc.20tactic.20comes.20to.20Lean4 --- - [x] depends on: #11960 [](https://gitpod.io/from-referrer/)

refactor: redefine `Finsupp` as `abbrev` of `DFinsupp`

2

--- - [ ] depends on: #13025 [](https://gitpod.io/from-referrer/)

--- [](https://gitpod.io/from-referrer/)

perf: improves the performance of the `Repr (Equiv.Perm α)` instance

2

--- [](https://gitpod.io/from-referrer/)

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Unscoping.20big.20operators Also, we change the notation for [`CategoryTheory.Limits.piObj`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/Products.html#CategoryTheory.Limits.piObj) from `∏ f` to `∏ᶜ f`. --- [](https://gitpod.io/from-referrer/)

refactor: change the format of `Repr (Equiv.Perm α)` from `{c[0, 1], c[2, 3]}` to `c[0, 1] * c[2, 3]`

1

--- - [ ] depends on: #12610 [](https://gitpod.io/from-referrer/)

refactor(Mathlib/Data/Seq/Seq): make `Seq'.mem_rec_on` more useful

3

```lean theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s) (h1 : ∀ b s', a = b ∨ C s' → C (cons...

feat(Mathlib/Data/Seq/Seq): prove `∀ a ∈ (s : Seq' α), p a` using coinduction

3

--- - [ ] depends on: #13509 This PR consists [Continued fractions makes an isomorphism between irrationals and baire space ](https://github.com/users/Komyyy/projects/3/) project [](https://gitpod.io/from-referrer/)