Commits leanprover-community/mathlib

Merge branch 'fg-surj' into fg-computations

mlavrent committed 3 years ago

65918573

Merge branch 'master' into fg-computations

mlavrent committed 3 years ago

8a7f2e35

feat(group_theory/index): Add `index_eq_zero_of_relindex_eq_zero` (#16991)

tb65536 committed 3 years ago

08b57a55

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719)

j-loreaux committed 3 years ago

63ff4532

feat(data/nat/choose/multinomial): add multinomial theorem (#16317)

pimotte committed 3 years ago

c9e2f055

feat(measure_theory/group/measure): generalise `is_haar_measure_map` slightly. (#17107)

ocfnash committed 3 years ago

62dabb94

feat(analysis/schwartz_space): Delta distribution (#16638)

mcdoll committed 3 years ago

b251b44a

feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition (#16596)

hrmacbeth committed 3 years ago

f333194f

feat: add warning to scripts/port_status.py (#17132)

kim-em committed 3 years ago

ddfa266e

feat(algebraic_geometry/morphisms/universally_closed): Define universally closed morphism between schemes (#17117)

erdOne committed 3 years ago

434e2fd2

feat(ring_theory/ideal/local_ring): add lemmas about and bundled versions of `local_ring.residue_field.map` (#17104)

mkaratarakis committed 3 years ago

18b538a7

feat(src/algebraic_geometry/morphisms/quasi_separated): Define quasi-separated morphisms. (#17080)

erdOne committed 3 years ago

558f5830

feat(ring_theory/derivation): The Kähler differential module is functorial (#17018)

erdOne committed 3 years ago

cceedbca

feat(number_theory/padics/padic_numbers): add is_fraction_ring instance (#16981)

mariainesdff committed 3 years ago

082350f2

feat(data): port finsupp.ne_locus/lex to dfinsupp (#16777)

alreadydone committed 3 years ago

99d31295

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

urkud committed 3 years ago

3882aaf6

feat(data/complex/module): add instance `complex.distrib_smul` (#17115)

astrainfinita committed 3 years ago

a923261c

feat(tactic/rcases.lean): `@⟨p1, p2⟩` patterns in `rcases` (#16617)

digama0 committed 3 years ago

356447fe

refactor(data/polynomial/degree): use `with_bot.unbot'` instead of `option.get_or_else` (#17120)

urkud committed 3 years ago

a15401cf

feat(topology/is_locally_homeomorph): Add `is_locally_homeomorph_on` (#17114)

tb65536 committed 3 years ago

36444798

feat(data/set/basic, topology/{subset_properties, connected}): A space is preconnected iff every continuous map to a discrete space is constant (#17070)

dagurtomas committed 3 years ago

0ca85a74

feat(analysis/convolution): prove associativity under more convenient assumptions (#16706)

fpvandoorn committed 3 years ago

1246edae

feat(data/finset/pointwise): allow lifting monoid homs to finsets (#16935)

b-mehta committed 3 years ago

cce4e962

feat(algebra/big_operators/norm_num): add limited support for finset intervals (#16518)

eric-wieser committed 3 years ago

f7953c0e

feat(data/enat/basic): add lemmas (#17118)

urkud committed 3 years ago

dbf8aa5f

refactor(topology/instances/discrete): refactor the proof of `discrete_topology.order_topology_of_pred_succ` to show an equivalence (#16831)

RemyDegenne committed 3 years ago

c82c2db1

feat(topology/continuous_function/algebra): functoriality of `C(⬝, A)` into star algebras. (#16817)

j-loreaux committed 3 years ago

2e83666b

feat(topology/algebra/module/locally_convex): generalize `disjoint.exists_open_convexes` to locally convex spaces (#16749)

ADedecker committed 3 years ago

083202d6

feat(analysis/special_functions/trigonometric/inverse): `arccos_pos`, `arccos_lt_pi_div_two` (#17111)

jsm28 committed 3 years ago

44682c2d

chore(order/*): golf 2 proofs (#17095)

urkud committed 3 years ago

0437938e