Commits leanprover-community/mathlib

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

chore(data/finset/pointwise): `{a} • t = a • t` (#17072)

YaelDillies committed 3 years ago

a2a19634

feat(topology/metric_space/basic): Distance between constant functions (#16958)

YaelDillies committed 3 years ago

3798ca1d

feat(order/directed): A few more lemmas (#16953)

YaelDillies committed 3 years ago

34826f0d

chore(order/filter/*): golf `ultrafilter.exists_ultrafilter_of_finite_inter_nonempty` (#17096)

urkud committed 3 years ago

3fbddc20

feat(category_theory/morphism_property): Define `morphism_property.universally`. (#17112)

erdOne committed 3 years ago

7dff92aa

feat(topology/continuous_on): Continuity on an open (#17089)

YaelDillies committed 3 years ago

54349530

chore(data/nat/enat): move into a subfolder (#17106)

urkud committed 3 years ago

8005d575