mathlib

mathlib copied to clipboard

feat(algebraic_geometry/projective_spectrum/scheme): add an equivalent definition of `from_Spec.carrier`

2

This is definition "computes better", so it is needed when showing `from_Spec` and `to_Spec` are inverses - [x] depends on: #16693 --- [](https://gitpod.io/from-referrer/)

jjaassoonn

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`. *...

urkud

feat(category_theory/abelian/transfer): adjoint functor transfers "enough-injectiveness"

1

If $A, B$ are abelian categories and $L\dashv R$ is a pair of adjoint functors, where $L$ is faithful and exact, then enough invectiveness of $B$ implies that of $A$...

jjaassoonn

feat(analysis/inner_product_space/spectrum): add a decomposition instance

1

This proof felt a bit painful - I suspect most of the results I needed already exist somewhere else. This `decomposition` instances inherits the noncomputability of `orthogonal_projection`, but it is...

eric-wieser

refactor(number_theory/divisors): redefine nat.divisors as a monoid hom

1

`nat.divisors` unconditionally preserves multiplication, so this bundles it as a monoid hom, similar for `nat.divisors_antidiagonal`. This PR also changes `nat.divisors` to be defined in terms of `nat.divisors_antidiagonal`, which drastically simplifies...

b-mehta

refactor(tactic/wlog): simplify and speed up `wlog`

25

Benefits: - The tactic is faster - The tactic is easier to port to Lean 4 Downside: - The tactic doesn't do any heavy-lifting for the user Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/wlog/near/296996966...

jcommelin

ADedecker

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n`

2

This PR adds: - Group instance for `π_(n+1)` - Commutative group instance for `π_(n+2)` --- - [x] depends on: #16879 [](https://gitpod.io/from-referrer/)

ralvrz

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

YaelDillies

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

1

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

j-loreaux