leanprover-community/mathlib

Pull Requests Commits

trying to resolve module docstring missing

laughinggas committed 2 years ago

324e0a14

laughinggas committed 2 years ago

cd8a28b6

laughinggas committed 2 years ago

6b1786d4

chore(linear_algebra/dual): prove a lemma with rfl (#18444)

eric-wieser committed 2 years ago

5455cb0b

feat(algebra/continued_fractions/*): add some API lemmas (#18434)

MichaelStollBayreuth committed 2 years ago

10d88727

feat(algebra/algebra/operations): the semiring of submodules over an algebra is idempotent (#18400)

eric-wieser committed 2 years ago

2bbc7e38

feat(combinatorics/simple_graph/connectivity): `concat` and `concat_rec` (#17209)

kmill committed 2 years ago

13cd3e89

feat(algebra/order/field/basic): `a ≤ b / c → a * c ≤ b` (#18367)

YaelDillies committed 2 years ago

5a82b067

split(topology/algebra/infinite_sum): Split into four files (#18414)

YaelDillies committed 2 years ago

32253a1a

chore(set_theory/ordinal/arithmetic): move power and logarithm to a new file (#18441)

eric-wieser committed 2 years ago

f1e061e3

feat (analysis/special_functions): limit formula and reflection formula for Gamma (#18404)

loefflerd committed 2 years ago

372edc36

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

leanprover-community-bot committed 2 years ago

1ead2234

chore(algebra/group/units): is_add_unit.decidable (#18439)

pechersky committed 2 years ago

369525b7

feat(analysis/fourier): Basic framework for Fourier transforms (#18428)

loefflerd committed 2 years ago

a231f964

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

leanprover-community-bot committed 2 years ago

ac34df03

refactor(combinatorics/configuration): Refactor `projective_plane` to extend `has_points` and `has_lines` (#18436)

tb65536 committed 2 years ago

26c71658

chore(algebra/quaternion): generalize the algebra instance (#18382)

eric-wieser committed 2 years ago

48085f14

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

leanprover-community-bot committed 2 years ago

34ee86e6

chore(algebra/algebra/basic): missing lemmas about the `↑` spelling of `algebra_map` (#18422)

eric-wieser committed 2 years ago

4ea65cad

feat(algebra/big_operators/basic): `finset.sum` under `mod` (#18364)

YaelDillies committed 2 years ago

6c5f73fd

chore(analysis/convex/specific_functions): remove unused import (#18431)

RemyDegenne committed 2 years ago

74e62ed9

chore(order/filter/filter_product): fix `const_lt`, make `const_lt_iff` `@[simp, norm_cast]` (#17442)

astrainfinita committed 2 years ago

3592f45e

refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICULAR instead of ⊥ UP TACK (#18423)

eric-wieser committed 2 years ago

70a4f219

chore(data/finset/sym): fix a typo (#18426)

xroblot committed 2 years ago

99624c1a

chore(algebra/algebra/basic): remove a duplicate lemma (#18415)

eric-wieser committed 2 years ago

71150516

feat(topology/continuous_function): lemmas on infinite sums of continuous functions (#18424)

loefflerd committed 2 years ago

ddbfecf5

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

leanprover-community-bot committed 2 years ago

ad0089ac

feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers (#18200)

eric-wieser committed 2 years ago

806c0bb8

chore(algebra/group_with_zero/units/lemmas): `div_div_cancel_left'` (#18421)

eric-wieser committed 2 years ago

dc6c365e

feat(algebraic_geometry/elliptic_curve/point): define addition of K-rational points (#17194)

Multramate committed 2 years ago

67f92b6f

Older