leanprover-community/mathlib3

Pull Requests Commits

Revert "minor edits"

JakobScholbach committed 4 years ago

aaf18fb6

JakobScholbach committed 4 years ago

cd8ac0ce

simplification lemmas in arrow.lean,

JakobScholbach committed 4 years ago

f6162978

minor simplifications

JakobScholbach committed 4 years ago

77a0c0da

add helper lemma to arrow.lean

JakobScholbach committed 4 years ago

668713d0

completely undo the edits in arrow.lean

JakobScholbach committed 4 years ago

aeb1e981

Revert edits at arrow.lean

JakobScholbach committed 4 years ago

799d7396

Copyedits at lifting_property, suggested changes by Scott Morrison in category_theory/arrow.lean

JakobScholbach committed 4 years ago

429ca239

JakobScholbach committed 4 years ago

86f105b0

create a new file about lifting properties

JakobScholbach committed 4 years ago

24433a84

feat(tactic/lint): linter for @[class] def (#6061)

digama0 committed 4 years ago

b4373e5a

chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra (#6800)

eric-wieser committed 4 years ago

a7563333

chore(*): removing some completed TODOs (#6844)

kim-em committed 4 years ago

144e9c4b

chore(category_theory/triangulated): cleanup (#6827)

kim-em committed 4 years ago

67730166

feat(algebra/category): subobjects in the category of R-modules (#6842)

TwoFX committed 4 years ago

beb2cc98

chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652)

kim-em committed 4 years ago

935003eb

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

leanprover-community-bot committed 4 years ago

e0a79186

feat(logic/basic): `is_trans Prop iff` instance (#6836)

gebner committed 4 years ago

94a4a958

doc(topology/sheaves/presheaf_of_functions): fix some documentation t… (#6835)

justus-springer committed 4 years ago

a008609d

feat(algebraic_geometry/prime_spectrum): prime spectrum analogue of Hilberts Nullstellensatz (#6805)

justus-springer committed 4 years ago

36fc1cab

feat(topology/algebra/continuous_functions): separates points (#6783)

kim-em committed 4 years ago

12170e2a

fix(algebraic_topology): added FQNs to simplicial locale (#6838)

ashwiniyengar committed 4 years ago

fd5f4333

feat(data/indicator_function): eq_self_of_superset (#6829)

benjamindavidson committed 4 years ago

ee5e9fb1

feat(algebra/category): add more variants of Module.as_hom (#6822)

TwoFX committed 4 years ago

aadd853d

feat(combinatorics/quiver): every connected graph has a spanning tree (#6806)

dwarn committed 4 years ago

b6e4d0b9

feat(data/multiset/basic): generalize rel.mono, rel_map (#6771)

Ruben-VandeVelde committed 4 years ago

315faac5

fix(data/complex/module): kill a non-defeq diamond (#6760)

sgouezel committed 4 years ago

9cda1ff6

chore(field_theory/splitting_field): module doc and generalise one lemma (#6739)

Julian-Kuelshammer committed 4 years ago

9893a260

feat(data/polynomial/bernstein): identities (#6470)

kim-em committed 4 years ago

c521336d

feat(combinatorics/simple_graph): degree lemmas (#5966)

b-mehta committed 4 years ago

edfe7e1e

Older