Commits leanprover-community/mathlib

feat(ring_theory/unique_factorization_domain): some lemmas relating shapes of factorisations (#9345)

Paul-Lez committed 3 years ago

8c89ae6f

doc(src/tactic/doc_commands): typo “between” → “better” (#12804)

nomeata committed 3 years ago

0c52d3b4

doc(archive/100-theorems-list/9_area_of_a_circle): fix `×` (#12803)

ericrbg committed 3 years ago

d3703fe9

chore(model_theory/definability): Change variable order in definability (#12802)

awainverse committed 3 years ago

f4e7f82a

feat(order/rel_iso): Add `subrel` instances (#12758)

vihdzp committed 3 years ago

f6e85fc4

feat(set_theory/*): Redefine `sup f` as `supr f` (#12657)

vihdzp committed 3 years ago

fdd7e98c

feat(model_theory/terms_and_formulas): Atomic, Quantifier-Free, and Prenex Formulas (#12557)

awainverse committed 3 years ago

290ad757

feat(category_theory/abelian) : injective resolutions of an object in a category with enough injectives (#12545)

jjaassoonn committed 3 years ago

d17ecf9e

feat(model_theory/terms_and_formulas): Language maps act on terms, formulas, sentences, and theories (#12609)

awainverse committed 3 years ago

80b8d191

feat(archive/100-theorems-list): add proof of thm 81 (#7274)

manuelcandales committed 3 years ago

bf690dd3

feat(data/nat/prime): add two lemmas with nat.primes, mul and dvd (#12780)

adomani committed 3 years ago

b49bc778

fix(ring_theory/power_series/basic): remove duplicate instance (#12744)

kbuzzard committed 3 years ago

5a547aa9

feat(number_theory/arithmetic_function): add eq of multiplicative functions (#12689)

khwilson committed 3 years ago

14ee5e03

feat(measure_theory/group/action): add `null_measurable_set.smul` (#12793)

urkud committed 3 years ago

ee8db20e

refactor(data/list/big_operators): review API (#12782)

urkud committed 3 years ago

2541387e

chore(algebraic_geometry/prime_spectrum/basic): remove TODO (#12768)

jjaassoonn committed 3 years ago

241d63d8

feat(group_theory/index): Intersection of finite index subgroups (#12776)

tb65536 committed 3 years ago

cfa7f6af

refactor(topology/algebra/field): make `topological_division_ring` extend `has_continuous_inv₀` (#12778)

j-loreaux committed 3 years ago

5ecd27ad

doc(overview): some additions to the Analysis section (#12791)

mcdoll committed 3 years ago

a7cad675

feat(analysis/*): generalize `set_smul_mem_nhds_zero` to topological vector spaces (#12779)

mcdoll committed 3 years ago

a32d58ba

chore(data/matrix/block): Do not print `matrix.from_blocks` with dot notation (#12774)

eric-wieser committed 3 years ago

adcfc58d

feat(algebra/pointwise): Subtraction/division of sets (#12694)

YaelDillies committed 3 years ago

cf8c5ff1

feat(model_theory/terms_and_formulas): Casting and lifting terms and formulas (#12467)

awainverse committed 3 years ago

32e5b6b9

feat(analysis/normed_space/basic): add `normed_division_ring` (#12132)

j-loreaux committed 3 years ago

a26dfc4c

chore(topology/algebra/group_with_zero): mark `has_continuous_inv₀` as a `Prop` (#12770)

j-loreaux committed 3 years ago

2cb5edb5

feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767)

eric-wieser committed 3 years ago

3e6e34e4

docs(algebra/order/floor): Update floor_semiring docs to reflect it's just an ordered_semiring (#12756)

khwilson committed 3 years ago

6bfbb49e

feat(data/nat/sqrt_norm_num): norm_num extension for sqrt (#12735)

digama0 committed 3 years ago

ca80c8b0

feat(algebraic_geometry/projective_spectrum) : lemmas about `vanishing_ideal` and `zero_locus` (#12730)

jjaassoonn committed 3 years ago

e944a998

chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771)

hrmacbeth committed 3 years ago

a1bdaddf