leanprover-community/mathlib3

Pull Requests Commits

Drop a lemma, add a lemma

urkud committed 2 years ago

f88ff5b1

urkud committed 2 years ago

5b9976dd

Merge branch 'master' into YK-comap-ite

urkud committed 2 years ago

f8dfa00d

feat(algebra/order/to_interval_mod): symmetric variants of lemmas (#18942)

eric-wieser committed 2 years ago

4c8f86bd

chore(algebra/order/lattice_group): remove redundant instance (#18951)

kim-em committed 2 years ago

db07e6fe

feat(order/category): Forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` (#18948)

YaelDillies committed 2 years ago

fa4a805d

doc(measure_theory): Fix some names and docstrings (#18910)

Felix-Weilacher committed 2 years ago

3905fa80

feat(number_theory/number_field/units): add is_unit_iff_norm (#18866)

xroblot committed 2 years ago

00f91228

chore(data/is_R_or_C/basic): rename `conj_mul_eq_norm_sq_left` to `conj_mul` (#18939)

urkud committed 2 years ago

25580801

feat(field_theory/intermediate_field): Add lemma for the `field_range` of `val` (#18940)

tb65536 committed 2 years ago

efed3cad

chore(number_theory/modular_forms/slash_invariant_forms): golf and rename (#18933)

eric-wieser committed 2 years ago

738054fa

feat(ring_theory/localization/away) : Add `num_denom` section (#18830)

faenuccio committed 2 years ago

570e9f48

chore(ring_theory/derivation): generalize tower instance (#18937)

eric-wieser committed 2 years ago

26ae6f67

chore(ring_theory/ideal/quotient): add missing smul compatibility instances (#18934)

eric-wieser committed 2 years ago

2f39bcbc

feat(data/is_R_or_C/basic): drop 2 fields, golf (#18931)

urkud committed 2 years ago

338fe44f

chore(probability/kernel/basic): make the function argument of kernel.deterministic explicit (#18930)

RemyDegenne committed 2 years ago

caf83ba4

chore(probability/kernel/composition): swap the order of the arguments of prod_mk_left (#18929)

RemyDegenne committed 2 years ago

698c80e9

chore(analysis/inner_product_space/basic): golf the proof of Cauchy-Schwarz (#18938)

urkud committed 2 years ago

07992a1d

feat(field_theory/ax_grothendieck): Ax-Grothendieck for algebraic extensions of finite fields (#18479)

ChrisHughes24 committed 2 years ago

4e529b03

chore(*): add mathlib4 synchronization comments (#18923)

leanprover-community-bot committed 2 years ago

fe8d0ff4

chore(analysis/normed_space/extend): golf, add aux lemmas (#18927)

urkud committed 2 years ago

aa1dbeab

chore(*): removed unneeded imports (#18926)

kim-em committed 2 years ago

f0c8bf92

chore(ring_theory/kaehler): extract from `ring_theory/derivation` (#18935)

eric-wieser committed 2 years ago

73f96237

chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#18928)

urkud committed 2 years ago

92c69b77

feat(measure_theory/constructions/prod): marginal measures (#18915)

RemyDegenne committed 2 years ago

726d2fe4

chore(ring_theory/discrete_valuation_ring): create folder ring_theory/discrete_valuation_ring (#18867)

faenuccio committed 2 years ago

c163ec99

feat(representation_theory/group_cohomology/basic): add standard definition of group cohomology (#18341)

Amelia Livingston committed 2 years ago

ef997baa

chore(data/set/intervals/monotone): fix names (#18924)

urkud committed 2 years ago

4d06b17a

chore(analysis/normed_space/basic): rename `abs_norm_eq_norm` to `abs_norm` (#18921)

urkud committed 2 years ago

f9dd3204

chore(data/{complex,is_R_or_C}/basic): fix name of `eq_conj_iff_*` lemmas (#18922)

eric-wieser committed 2 years ago

caa58cbf

Older