leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/adjunction): construct an adjunction on the over category (#7290)

b-mehta committed 4 years ago

55a1e65b

chore(category_theory/subterminal): update docstring (#7289)

b-mehta committed 4 years ago

d9df8fb5

feat(data/nat/prime): nat.factors_eq_nil and other trivial simp lemmas (#7284)

eric-wieser committed 4 years ago

07e9dd4c

chore(.github/workflows): add delegated tag on comment (#7251)

bryangingechen committed 4 years ago

6deafc20

feat(topology/continuous_function): change formulation of separates points strongly (#7248)

kim-em committed 4 years ago

f68645f1

chore(topology/algebra/affine): add @continuity to line_map_continuous (#7246)

kim-em committed 4 years ago

22f96fc0

feat(geometry/euclidean): proof of Freek thm 55 - product of chords (#7139)

manuelcandales committed 4 years ago

afa6b72e

feat(analysis/special_functions/bernstein): Weierstrass' theorem: polynomials are dense in C([0,1]) (#6497)

kim-em committed 4 years ago

dac1da3a

fix(data/{finsupp,polynomial,mv_polynomial}/basic): add missing decidable arguments (#7309)

eric-wieser committed 4 years ago

f2984d51

feat(data/list/zip): map_zip_with (#7295)

pechersky committed 4 years ago

120be3d9

feat(analysis/normed_space/dual): generalize to seminormed space (#7262)

riccardobrasca committed 4 years ago

253d4f5b

feat(analysis/special_functions/integrals): integral_comp for `f : ℝ → ℝ` (#7216)

benjamindavidson committed 4 years ago

700d4773

feat(order/complete_lattice): independence of an indexed family (#7199)

kbuzzard committed 4 years ago

721e0b9e

chore(tactic/elementwise): fixes (#7188)

kim-em committed 4 years ago

66220ac0

doc(data/quot): promote a comment to a docstring (#7306)

eric-wieser committed 4 years ago

f08fe5fd

feat(data/dfinsupp): copy map_range defs from finsupp (#7293)

eric-wieser committed 4 years ago

7db1181e

feat(data/finset/lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275)

eric-wieser committed 4 years ago

80028f3a

feat(category_theory/monoidal): Drinfeld center (#7186)

kim-em committed 4 years ago

9b8d6e49

refactor(order/well_founded_set): partially well ordered sets using relations other than `has_le.le` (#7131)

awainverse committed 4 years ago

923314f2

feat(group_theory/{order_of_element, perm/cycles}): two cycles are conjugate iff their supports have the same size (#7024)

awainverse committed 4 years ago

02a31338

feat(algebra/algebra/basic): add alg_hom.apply (#7278)

eric-wieser committed 4 years ago

8481bf46

feat(algebra/big_operators): product over coerced fintype (#7236)

b-mehta committed 4 years ago

4abf9618

refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227)

eric-wieser committed 4 years ago

ad588611

feat(algebraic_geometry/prime_spectrum): More lemmas (#7244)

justus-springer committed 4 years ago

9bdc5551

feat(logic/basic): exists_or_eq_{left,right} (#7224)

pechersky committed 4 years ago

39d23b8e

feat(linear_algebra/bilinear_form): Unique adjoints with respect to a nondegenerate bilinear form (#7071)

kex-y committed 4 years ago

bf22ab3f

feat(category_theory/subobject): easy facts about the top subobject (#7267)

TwoFX committed 4 years ago

a4f59bde

feat(algebra/lie/abelian): expand API for `lie_module.maximal_trivial_submodule` (#7235)

ocfnash committed 4 years ago

0c721d5d

chore(combinatorics/quiver): make quiver a class (#7150)

kim-em committed 4 years ago

944ffff9

feat(category_theory/abelian): definition of projective object (#7108)

kim-em committed 4 years ago

5e188d2f

Newer Older