leanprover-community/mathlib

Pull Requests Commits

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

lint(*): split long lines (#6833)

urkud committed 4 years ago

61ed14e2

refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831)

riccardobrasca committed 4 years ago

78034350

feat(category_theory/subobject): API for working with inequalities (#6818)

TwoFX committed 4 years ago

489f5225

feat(data/fintype/basic): add decidable_mem_range_fintype (#6817)

eric-wieser committed 4 years ago

736b1e81

feat(group_theory/subgroup): add {monoid,add_monoid,ring}_hom.lift_of_right_inverse (#6814)

eric-wieser committed 4 years ago

c2e9ec02

chore(algebra/group/basic): dedup, add a lemma (#6810)

urkud committed 4 years ago

5cafdfff

feat(ring_theory/polynomial/homogenous): add a `direct_sum.gcomm_monoid` instance (#6825)

eric-wieser committed 4 years ago

94f59d8b

refactor(tactic/ring): split off `ring_nf` tactic (#6792)

digama0 committed 4 years ago

9f56a0bf

feat(data/support): add `function.mul_support` (#6791)

urkud committed 4 years ago

a0a21774

feat(linear_algebra): composing with a linear equivalence does not change the image (#6816)

TwoFX committed 4 years ago

ffca31af

feat(data/finsupp/basic): add `can_lift (α → M₀) (α →₀ M₀)` (#6777)

urkud committed 4 years ago

e54f6339

feat(algebra/group/type_tags): adding function coercion for `additive` and `multiplicative` (#6657)

ashwiniyengar committed 4 years ago

480b00c8

feat(linear_algebra/dual): add dual_annihilator_sup_eq_inf_dual_annihilator (#6808)

kex-y committed 4 years ago

0b543c34

feat(algebra/subalgebra): missing norm_cast lemmas about operations (#6790)

kim-em committed 4 years ago

f3a4c480

Newer Older