Commits leanprover-community/mathlib3

Merge branch 'master' into eric-wieser/derivation-bimodule

eric-wieser committed 2 years ago

Verified 6e62506c

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

Merge branch 'eric-wieser/derivation-tower-instance' into eric-wieser/derivation-bimodule

eric-wieser committed 2 years ago

b10c52ab

feat(ring_theory/derivation): support non-commutative rings (via bimodules)

eric-wieser committed 2 years ago

8fafd524

chore(ring_theory/derivation): generalize tower instance

eric-wieser committed 2 years ago

84326cdb

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

feat(probability/kernel/composition): add a notation for the product of kernels (#18918)

RemyDegenne committed 2 years ago

15e02bcd

chore(ring_theory/polynomial/quotient): remove spurious restrict_scalars (#18916)

kim-em committed 2 years ago

61d8b824

refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` (#18912)

eric-wieser committed 2 years ago

645b6de4

feat(data/mv_polynomial/basic): add and generalize some lemmas from finsupp and monoid_algebra (#18855)

Hagb committed 2 years ago

f69db8ce

feat(analysis/special_functions): file for evaluations of specific improper integrals (#18821)

loefflerd committed 2 years ago

ec452806

feat(data/list/cycle): well-founded or transitive irreflexive relations don't have cycles (#18512)

vihdzp committed 2 years ago

7413128c

feat(algebra/algebra/basic): add shortcut instance (#18907)

Ruben-VandeVelde committed 2 years ago

36b8aa61

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

leanprover-community-bot committed 2 years ago

ef553359