leanprover-community/mathlib3

Pull Requests Commits

finish finsupp.basic

pechersky committed 3 years ago

da5d3173

eric-wieser committed 3 years ago

d13d0303

feat(set_theory/zfc/basic): `⊆` is reflexive, transitive, antisymmetric (#15551)

vihdzp committed 3 years ago

a1a1fbd7

chore(probability_mass_function/uniform): Move some constructions to a new file (#15500)

dtumad committed 3 years ago

7ee53e0f

feat(set_theory/zfc/basic): add `refl`, `symm`, `trans` attributes to `equiv` lemmas (#15549)

vihdzp committed 3 years ago

40e77914

refactor(data/nat/part_enat): move `complete_linear_order` instance (#15543)

urkud committed 3 years ago

e2e097cc

refactor(data/dfinsupp/basic): Improve definitional equalities of coercions (#15521)

eric-wieser committed 3 years ago

327259af

feat(category_theory/shapes/pullbacks): Pullbacks isomorphic to the opposite of pushouts (#15455)

erdOne committed 3 years ago

dcb4b68a

feat(field_theory/intermediate_field): `dsimp` lemma (#15188)

YaelDillies committed 3 years ago

4359e481

feat(combinatorics/simple_graph/trails): Euler's condition for trails (#15158)

kmill committed 3 years ago

edaaaa4a

feat(data/nat/factorization/basic): add lemma `factorization_eq_card_pow_dvd` (#15014)

stuart-presnell committed 3 years ago

261c24c6

feat(ring_theory/derivation): Derivations into square-zero ideals corresponds to liftings. (#15244)

erdOne committed 3 years ago

ffc640f4

feat(analysis/inner_product_space/[pi_L2, l2_space]): compute inner product in a given [orthonormal, hilbert] basis (#15514)

ADedecker committed 3 years ago

73e41c24

feat(data/list): accessing list with fallback (#15138)

pechersky committed 3 years ago

be93cace

chore(topology/algebra): cleanup (#15301)

urkud committed 3 years ago

c31b1f3d

feat(set_theory/zfc/ordinal): transitive sets (#15288)

vihdzp committed 3 years ago

7059323d

refactor(data/set/countable): rename some lemmas (#15527)

urkud committed 3 years ago

54cb8484

feat(logic/encodable/basic): an encodable type is countable (#15524)

urkud committed 3 years ago

df2ebcff

chore(analysis/locally_convex/with_seminorms): change `with_seminorms` to a structure (#15388)

mcdoll committed 3 years ago

cfc157d3

feat(tactic/linear_combination): allow linear_combination to leave goal open (#15319)

robertylewis committed 3 years ago

71786433

chore(data/buffer/parser/numeral): new int and rat parsers don't need to be meta (#15535)

alexjbest committed 3 years ago

2220b0cb

ci(.github/workflows/*): Make build step fail if lean returns nonzero value (#15520)

bentoner committed 3 years ago

3c33aba3

refactor(logic/equiv/nat): remove `equiv.nat_prod_nat_equiv_nat` (#15509)

urkud committed 3 years ago

3788b073

feat(ring_theory/valuation): Properties of valuation rings. (#15093)

erdOne committed 3 years ago

4d352641

feat(set_theory/ordinal/arithmetic): `pred 0 = 0` (#15533)

vihdzp committed 3 years ago

7c916a69

chore(probability/probability_mass_function): move folder into probability (#15525)

kex-y committed 3 years ago

be6a4082

feat(data/list/basic): when drop_while and take_while hold (#15472)

pechersky committed 3 years ago

df5297aa

refactor(algebra/punit_instances): Move order instances (#15465)

YaelDillies committed 3 years ago

5306f2df

feat(data/nat/basic): add recursion principle `even_odd_rec` as a wrapper around `binary_rec` (#15457)

stuart-presnell committed 3 years ago

6e8c150a

feat(set_theory/ordinal/arithmetic): more log lemmas (#15447)

vihdzp committed 3 years ago

5e114a3e

Older