Commits leanprover-community/mathlib

rat but moreso

eric-wieser committed 3 years ago

551b58fc

wip

eric-wieser committed 3 years ago

a4558132

fix

eric-wieser committed 3 years ago

bcc9e98b

fix blank line

eric-wieser committed 3 years ago

fc42704c

authorship

eric-wieser committed 3 years ago

48fc050b

feat(analysis/normed_space/exponential): Generalize `field` lemmas about `exp 𝕂 𝕂` to `division_ring` lemmas about `exp 𝕂 𝔸`

eric-wieser committed 3 years ago

9c7f0987

feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)

yuma-mizuno committed 3 years ago

8f116f43

chore(analysis/normed_space/exponential): Make the `𝔸` argument implicit (#13986)

eric-wieser committed 3 years ago

27e105d2

feat(number_theory/legendre_symbol/*): add results on value at -1 (#13978)

MichaelStollBayreuth committed 3 years ago

eea16dc8

feat(data/polynomial/laurent): laurent polynomials -- defs and some API (#13784)

adomani committed 3 years ago

dfe1897f

feat(tactic/lint/misc): adding a linter that flags iffs with explicit variables on both sides (#11606)

arthurpaulino committed 3 years ago

58d83ed5

docs(ring_theory/localization/ideal): fix an unused name (#13992)

yuma-mizuno committed 3 years ago

863a1676

chore(data/zmod/basic.lean): change order of arguments of `zmod.nat_cast_mod` for consistency (#13988)

MichaelStollBayreuth committed 3 years ago

db5c2a6d

refactor(set_theory/game/pgame): Remove `pgame.omega` (#13960)

vihdzp committed 3 years ago

40bedd62

feat(set_theory/game/pgame): Add remark on relabelings (#13732)

vihdzp committed 3 years ago

c9f5cee2

feat(measure_theory/function/conditional_expectation): induction over Lp functions which are strongly measurable wrt a sub-sigma-algebra (#13129)

RemyDegenne committed 3 years ago

ba627bc7

docs(data/polynomial/algebra_map): fix a typo in a doc-string (#13989)

adomani committed 3 years ago

fe0c4cd9

feat(linear_algebra/matrix/nonsingular_inverse): inverse of a diagonal matrix is diagonal (#13827)

eric-wieser committed 3 years ago

f6c030fe

feat(probability/stopping): add properties of the measurable space generated by a stopping time (#13909)

RemyDegenne committed 3 years ago

e4d3d339

feat(topology/algebra/monoid): add missing `has_continuous_const_smul` instances (#13987)

eric-wieser committed 3 years ago

f0339374

feat(analysis/asymptotics/asymptotics): add `is_O.exists_mem_basis` (#13973)

urkud committed 3 years ago

97c4d4ed

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `mul_zero_class` `partial_order` / `linear_order` (#13377)

astrainfinita committed 3 years ago

d9893051

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `mul_zero_one_class` `partial_order` (#13375)

astrainfinita committed 3 years ago

1675b78d

feat(measure_theory/group/*): various lemmas about invariant measures (#13539)

fpvandoorn committed 3 years ago

95413e23

feat(analysis/special_functions/trigonometric): add a lemma (#13975)

urkud committed 3 years ago

ebac9f03

feat(model_theory/*): Any theory with infinite models has arbitrarily large models (#13980)

awainverse committed 3 years ago

faf16900

chore(algebra/ring/idempotents): golf iff_eq_zero_or_one (#13977)

Ruben-VandeVelde committed 3 years ago

f0eded9a

feat(algebra/group/defs): Division monoids (#13860)

YaelDillies committed 3 years ago

151933d1

feat(model_theory/skolem): Downward Löwenheim–Skolem (#13723)

awainverse committed 3 years ago

c62dfe61

feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858)

ADedecker committed 3 years ago

91cc3f06