Yury G. Kudryashov

You're talking about the bottom in 9.5.1 Zeroth Power, but don't discuss it in the next section, while it seems to make a difference here: besides the `unit` function, we...

* replace `*_hom.map_inv` by a generic lemma `map_inv₀` assuming `[monoid_with_zero_hom_class]`; * replace `*_hom.map_div` by a generic lemma `map_div₀` assuming `[monoid_with_zero_hom_class]`; * replace `*_hom.map_zpow` by a generic lemma `map_zpow₀` assuming `[monoid_with_zero_hom_class]`;...

[math-classes] Non-commutative (semi)rings

2

Currently MathClasses defines `Ring` to be a commutative ring. I propose to rename it to `CommutativeRing`, and introduce a `Ring` for non-commutative rings. Are there any objections? If no, I'll...

Sometimes I get errors like ``` /mathlib/src/data/set/intervals/disjoint.lean:36:14: error: type mismatch at application not_le.mpr hx.left.right term hx.left.right has type x < b but is expected to have type ?m_3 < ?m_4...

Make `@[trans]`/`calc` work with `homeomorph` etc

1

Here is a minimal non-working example. See also `homeomorph.trans` in `mathlib`. It seems that `calc` makes very strict assumptions on the meaning of implicit arguments preceding the explicit arguments of...

feat(group_theory/index): criterion for subgroups of index two

4

* A subgroup has index two if and only if there exists `a` such that for all `b`, `b * a ∈ H` is equivalent to `b ∉ H`. *...

* Generalize `card_fiber_eq_of_mem_range` to homomorphisms from a group to a monoid. * Rename it to `monoid_hom.card_fiber_eq_of_mem_range`, use `to_additive`. --- [](https://gitpod.io/from-referrer/)

chore(data/equiv/transfer_instance): avoid `let`, provide `nsmul`

1

Also use `@[simps]` to generate some lemmas. --- [](https://gitpod.io/from-referrer/)

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

feat(algebra/big_operators/finprod): assorted lemmas

1

--- These lemmas come from an old version of #8903. I don't need them anymore, so feel free to reject or drop some of the lemmas before merging. [![Open in...