leanprover-community/mathlib

Pull Requests Commits

Add computable inverses alongside surjectivity

eric-wieser committed 5 years ago

93a0ff0d

feat(ring_theory/ideal): Add lift_of_right_inverse which is computable

eric-wieser committed 5 years ago

11d44d1a

feat(group_theory/subgroup): Add lift_of_right_inverse which is computable

eric-wieser committed 5 years ago

24399402

feat(group_theory/subgroup): Define lift_of_surjective_equiv

eric-wieser committed 5 years ago

1431a2d2

doc(data/buffer/parser/basic): fix typo (#5792)

sorawee committed 5 years ago

9381e37d

chore(field_theory/minpoly): meaningful variable names (#5773)

jcommelin committed 5 years ago

8ab1a39d

feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703)

riccardobrasca committed 5 years ago

db617b3c

chore(category_theory/monad): golf and lint monadic adjunctions (#5769)

b-mehta committed 5 years ago

f3d3d046

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

leanprover-community-bot committed 5 years ago

3089b161

feat(data/option/*): pmap and pbind defs and lemmas (#5442)

pechersky committed 5 years ago

2f824aa1

refactor(algebra/monoid_algebra) generalize from group to monoid algebras (#5785)

Julian-Kuelshammer committed 5 years ago

c3639e94

refactor(analysis/calculus/deriv): simpler proof of `differentiable_at.div_const` (#5782)

Jesse Michael Han committed 5 years ago

f29d1c30

hack(manifold): disable subsingleton instances to speed up simp (#5779)

sgouezel committed 5 years ago

83d44a3d

doc(tactic/auto_cases): fix typo (#5784)

sorawee committed 5 years ago

bf46986e

feat(data/set/lattice): add lemmas set.Union_subtype and set.Union_of_singleton_coe (#5691)

adomani committed 5 years ago

289df3a7

chore(topology/metric_space/isometry): a few more lemmas (#5780)

urkud committed 5 years ago

2c4a5161

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

leanprover-community-bot committed 5 years ago

00e1f4c8

chore(group_theory/perm/{sign,cycles}): renaming for dot notation, linting, formatting (#5777)

bryangingechen committed 5 years ago

dec44fe7

chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771)

jcommelin committed 5 years ago

a2630fc3

feat(category_theory/is_filtered): is_filtered_of_equiv (#5485)

kl-i committed 5 years ago

0cc93a13

feat(measure_theory/haar_measure): Prove uniqueness (#5663)

fpvandoorn committed 5 years ago

787e6b30

chore(category_theory/limits): coproduct functor (#5677)

b-mehta committed 5 years ago

23373d15

refactor(data/nat/fib): explicitly state fibonacci sequence is monotone (#5776)

Julian-Kuelshammer committed 5 years ago

e0f4142e

refactor(linear_algebra/dual): replace dim<omega by finite_dimensional (#5775)

Julian-Kuelshammer committed 5 years ago

41556652

feat(category_theory/adjunction): reflective functors (#5680)

b-mehta committed 5 years ago

d23dbfba

feat(category_theory/sites): closed sieves (#5282)

b-mehta committed 5 years ago

64abe5aa

chore(topology/metric_space/gluing): use `⨅` notation (#5772)

urkud committed 5 years ago

e076a9c1

feat(linear_algebra/basic): add comap span lemmas (#5744)

ocfnash committed 5 years ago

ba5d1f63

feat(algebraic_geometry/prime_spectrum): add lemma zero_locus_bUnion (#5692)

adomani committed 5 years ago

bd578040

feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials (#5520)

dtumad committed 5 years ago

55d5564a

Older