leanprover-community/mathlib3

Pull Requests Commits

feat(set_theory/cardinal): Lift `min` and `max` (#12518)

vihdzp committed 4 years ago

0964573a

feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744)

nomeata committed 4 years ago

717b11ec

docs(algebra/group/hom): fix typo (#12723)

ericrbg committed 4 years ago

a50de33f

chore(number_theory/primorial): speed up some proofs (#12714)

Ruben-VandeVelde committed 4 years ago

35bb571b

feat(algebraic_geometry/projective_spectrum): basic definitions of projective spectrum (#12635)

jjaassoonn committed 4 years ago

a8bfcfed

feat(data/nat/fib): norm_num plugin for fib (#12463)

kmill committed 4 years ago

a7a2f9d4

feat(data/pnat/find): port over `nat.find` API (#12413)

pechersky committed 4 years ago

500a1d32

feat(group_theory/subsemigroup/basic): subsemigroups (#12111)

pechersky committed 4 years ago

bbc66b5e

chore(measure_theory/function): split files strongly_measurable and simple_func_dense (#12711)

sgouezel committed 4 years ago

50691e59

feat(ring_theory/fractional_ideal): two span_singleton lemmas (#12656)

Multramate committed 4 years ago

ba6c84dd

feat(algebra/group_power/order): add le_pow (#12436)

seangolinski7 committed 4 years ago

17c74f19

feat(topology/bornology/hom): Locally bounded maps (#12046)

YaelDillies committed 4 years ago

91f98e82

feat(set_theory/ordinal_arithmetic): A set of ordinals is bounded above iff it's small (#11870)

vihdzp committed 4 years ago

68033a22

feat(analysis/seminorm): three simple lemmas about balls (#12720)

mcdoll committed 4 years ago

a452bfa1

feat(algebra/parity + data/{int, nat}/parity): parity lemmas for general semirings (#12718)

adomani committed 4 years ago

1f1289fc

chore(scripts): update nolints.txt (#12728)

leanprover-community-bot committed 4 years ago

cbd61731

chore(data/equiv/basic): use `option.elim` and `sum.elim` (#12724)

urkud committed 4 years ago

45061f36

chore(algebra/associated): move prime_dvd_prime_iff_eq (#12706)

Ruben-VandeVelde committed 4 years ago

b622d4df

feat(group_theory/submonoid/operations): monoids are isomorphic to themselves as submonoids (#12658)

Multramate committed 4 years ago

7ed4f2ce

feat(algebra/algebra/subalgebra/pointwise): lemmas about `*` and `to_submodule` (#12695)

eric-wieser committed 4 years ago

375419f9

feat(linear_algebra/matrix/determinant): special case of the matrix determinant lemma (#12682)

eric-wieser committed 4 years ago

7582e149

feat(algebra/big_operators/finprod): finite product of power is power of finite product (#12655)

Multramate committed 4 years ago

9c09965e

doc(algebra/hierarchy_design): fix my name (#12674)

eric-wieser committed 4 years ago

88a59785

feat(linear_algebra/matrix/nonsingular_inverse): Add `matrix.list_prod_inv_reverse` (#12691)

eric-wieser committed 4 years ago

530f0088

fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680)

vihdzp committed 4 years ago

7a02c9e6

feat(linear_algebra/clifford_algebra/conjugation): add lemmas showing interaction between `involute` and `even_odd` (#12672)

eric-wieser committed 4 years ago

a3b39c6e

feat(group_theory/finiteness): quotient of fg is fg (#12652)

Multramate committed 4 years ago

48ffeb79

chore(category_theory/preadditive/projective_resolution): typo (#12702)

jjaassoonn committed 4 years ago

a98202b2

perf(analysis/convec/topology): remove topological_add_group.path_connected instance (#12675)

gebner committed 4 years ago

eefa4257

feat(model_theory/terms_and_formulas): Notation for terms and formulas from Flypitch (#12630)

awainverse committed 4 years ago

5b90340b

Newer Older