Commits leanprover-community/mathlib

Merge branch 'master' into SP_interval_monoid

stuart-presnell committed 3 years ago

ffa33fac

feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712)

stuart-presnell committed 3 years ago

14c52e99

chore(data.matrix): rename `minor` to `submatrix` (#16101)

abentkamp committed 3 years ago

55e2dfde

feat(ring_theory/etale): Condition for a quotient of a formally smooth algebra to be formally smooth. (#15842)

erdOne committed 3 years ago

eba35e3a

chore(scripts): update nolints.txt (#16117)

leanprover-community-bot committed 3 years ago

881d1ce9

chore(number_theory/cyclotomic/primitive_roots): generalisation linter (#16013)

ericrbg committed 3 years ago

32258e92

feat(field_theory/intermediate_field): Add `alg_hom.field_range` (#16078)

tb65536 committed 3 years ago

26c2c38d

feat(field_theory/normal): A compositum of normal extensions is normal (#16076)

tb65536 committed 3 years ago

551079b0

chore(ring_theory/graded_algebra/basic): golf `graded_ring.proj_zero_ring_hom` (#16081)

jjaassoonn committed 3 years ago

35f49417

feat(algebraic_geometry/morphisms): Construct morphism properties from ring homomorphism properties (#16059)

erdOne committed 3 years ago

ce566b31

feat(algebra/order/complete.field): add real.ring_hom_eq_id (#16049)

xroblot committed 3 years ago

61c8f89b

feat(number_theory): fundamental identity of ramification index and inertia degree (#12287)

Vierkantor committed 3 years ago

86db394f

feat(ring_theory/ring_hom/integral): Integral extensions are stable under base change. (#16094)

erdOne committed 3 years ago

40ac1b25

feat(linear_algebra/clifford_algebra/basic): invertibility of vectors (#16077)

eric-wieser committed 3 years ago

ffb51d35

feat(topology/basic): intersection of a finset-indexed open sets is open (#16075)

mcdoll committed 3 years ago

ae132cd6

feat(algebraic_geometry/morphisms): Condition for target affine locally to be stable under base change (#16061)

erdOne committed 3 years ago

4a0c4973

chore(group_theory/*): Fix lint (#16095)

YaelDillies committed 3 years ago

b78cf506

feat(ring_theory/derivation): Construction of the module of Kähler differentials. (#16047)

erdOne committed 3 years ago

753ef903

feat(group_theory/transfer): The transfer homomorphism `G →* center G` (#14520)

tb65536 committed 3 years ago

c30985dc

feat(linear_algebra/linear_pmap): introduce notation (#15751)

mcdoll committed 3 years ago

22dce611

feat(group_theory/group_action/defs): `additive`/`multiplicative` instances (#15719)

YaelDillies committed 3 years ago

4e76ad05

feat(data/nat/factorization/basic): define `ord_proj[p]` and `ord_compl[p]`, prove basic lemmas (#15589)

stuart-presnell committed 3 years ago

6c135283

feat(data/list/forall2): add `list.forall₂_iff_nth_le` (#16073)

madvorak committed 3 years ago

bb289539

feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism. (#15711)

erdOne committed 3 years ago

e83ba8f5

feat(data/polynomial): Polynomial modules (#15065)

erdOne committed 3 years ago

b6041198

refactor(order/rel_classes): redefine `is_well_order` in terms of `is_well_founded` (#15729)

vihdzp committed 3 years ago

08931580

chore(scripts): update nolints.txt (#16090)

leanprover-community-bot committed 3 years ago

f5de6ed7

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial` (#15889)

alreadydone committed 3 years ago

e14ff257

feat(algebra/order/ring): add some instances about covariance (#14763)

astrainfinita committed 3 years ago

64e20fb0

chore(combinatorics/simple_graph): review inhabited instances (#15770)

kmill committed 3 years ago

2303b3e2