leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 2 years ago

fa1e6b9a

improve docstring

vihdzp committed 2 years ago

beadb264

Update relation.lean

vihdzp committed 2 years ago

3916391c

feat(measure_theory/measurable_space): Cast of natural is measurable (#18676)

YaelDillies committed 2 years ago

88fcb83f

feat(combinatorics/additive/e_transform): e-transforms (#18683)

YaelDillies committed 2 years ago

207c9259

fix(data/nat/squarefree): `norm_num` only supports `squarefree` on naturals (#18708)

Vierkantor committed 2 years ago

3c1368ca

chore(algebra/order/lattice_group): Golf (#18046)

mans0954 committed 2 years ago

474656fd

feat(data/{set,finset}/pointwise): `a • t ⊆ s • t` (#18697)

YaelDillies committed 2 years ago

5e526d18

refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` (#15071)

vihdzp committed 2 years ago

210657c4

feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems (#2819)

alexjbest committed 2 years ago

02e095b2

feat(data/pnat/basic): pnat is a well-order (#18700)

vihdzp committed 2 years ago

172bf281

chore(analysis/locally_convex/strong_topology): generalize to semilinear maps (#18679)

mcdoll committed 2 years ago

47b12e7f

chore(*): Miscellaneous lemmas (#18677)

YaelDillies committed 2 years ago

29cb56a7

feat(order/rel_iso): well-founded instances for subtypes (#18699)

vihdzp committed 2 years ago

5923c4c7

refactor(data/matrix/basic): work around leanprover/lean4#2042 (#18696)

eric-wieser committed 2 years ago

3e068ece

refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140)

eric-wieser committed 2 years ago

ce11c3c2

refactor(analysis/inner_product_space): split `submodule.orthogonal` to a new file (#18706)

eric-wieser committed 2 years ago

6e272cd8

chore(category_theory): removed stupid example (#18701)

joelriou committed 2 years ago

94d4e70e

chore(category_theory/preadditive/projective): split out two lemmas to reduce imports (#18688)

kim-em committed 2 years ago

f8d8465c

chore(ring_theory/ideal/local_ring): move ring_equiv.local_ring into local_ring.lean (#18686)

kim-em committed 2 years ago

ec1c7d81

feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)

eric-wieser committed 2 years ago

d97a0c9f

feat(data/set/finite): When `s ×ˢ t` is finite (#18674)

YaelDillies committed 2 years ago

c941bb94

feat (number_theory/modular_forms): holomorphy of the Jacobi theta function (#18631)

loefflerd committed 2 years ago

fe44cd36

feat(data/list/lemmas): add lemmas about `set.range list.nth*` (#18647)

urkud committed 2 years ago

2ec920d3

chore(order/category): Partially revert categories (#18690)

Parcly-Taxel committed 2 years ago

71b36b6f

chore(algebra/star/self_adjoint): generalize a lemma to `semifield` (#18687)

eric-wieser committed 2 years ago

a6ece354

feat(analysis/calculus/cont_diff): bound for the iterated derivative of a product (#18632)

sgouezel committed 2 years ago

91862a60

refactor(representation_theory/group_cohomology_resolution): refactor `k[G^{n + 1}]` isomorphism (#18271)

Amelia Livingston committed 2 years ago

c04bc6e9

fix(algebra.group.ulift): fix to_additive name for cancel_comm_monoid (#18268)

rwbarton committed 2 years ago

564bcc44

feat(set_theory/zfc/basic): define Set and Class intersection (#18232)

vihdzp committed 2 years ago

229f6f14

Older