leanprover-community/mathlib3

Pull Requests Commits

refactor(order/preorder_hom): golf and simp lemmas (#7429)

b-mehta committed 4 years ago

97843966

feat(algebra/group/basic): prove `a / 1 = a` and remove `sub_zero` (#7956)

adomani committed 4 years ago

cbb8f019

feat(data/setoid/basic): add a computable version of quotient_ker_equiv_of_surjective (#7930)

eric-wieser committed 4 years ago

6578f1ce

refactor(ring_theory): use `x ∈ non_zero_divisors` over `x : non_zero_divisors` (#7961)

Vierkantor committed 4 years ago

1e43208e

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

leanprover-community-bot committed 4 years ago

1a6c871a

feat(data/matrix): `has_repr` instances for `fin` vectors and matrices (#7953)

Vierkantor committed 4 years ago

dc5d0c10

feat(model_theory/basic): Substructures (#7762)

awainverse committed 4 years ago

641a9d30

docs(data/option/basic): add module docstring (#7958)

YaelDillies committed 4 years ago

456a6d51

docs(data/set/disjointed): add module docstring and some whitespaces (#7957)

YaelDillies committed 4 years ago

08dfaab8

docs(data/*/nat_antidiagonal): add one module docstring and harmonise others (#7919)

YaelDillies committed 4 years ago

49aa1064

doc(topology/algebra/ring): add module docs + tidy (#7893)

ericrbg committed 4 years ago

366a4496

feat(data/list/cycle): cycles as quotients of lists (#7504)

pechersky committed 4 years ago

a564bf1e

refactor(geometry/manifold/instances/circle): split out (topological) group facts (#7951)

hrmacbeth committed 4 years ago

0490b432

chore(measure_theory/lp_space): simplify tendsto_Lp_iff_tendsto_\McLp by using tendsto_iff_dist_tendsto_zero (#7942)

RemyDegenne committed 4 years ago

95a116a1

refactor(algebra/algebra/basic): replace `algebra.comap` with `restrict_scalars` (#7949)

hrmacbeth committed 4 years ago

690ab173

feat(algebraic_geometry/Spec): Make Spec a functor. (#7790)

justus-springer committed 4 years ago

b8658928

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

leanprover-community-bot committed 4 years ago

ba3a4b7a

fix(measure_theory/interval_integral): generalize some lemmas (#7944)

benjamindavidson committed 4 years ago

30314c22

feat(order/iterate): id_le lemmas (#7943)

YaelDillies committed 4 years ago

45619c73

feat(analysis/convex/basic): a linear map is convex and concave (#7934)

YaelDillies committed 4 years ago

e5c97e10

feat(analysis/convex/basic): convex_on lemmas (#7933)

YaelDillies committed 4 years ago

f1f4c23f

feat(analysis/normed_space/dual): add eq_zero_of_forall_dual_eq_zero (#7929)

RemyDegenne committed 4 years ago

5d03dcd4

feat(data/finsupp/basic): equiv_congr_left (#7755)

digama0 committed 4 years ago

e5ff5fb4

feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927)

RemyDegenne committed 4 years ago

2f1f34a9

docs(undergrad): mark convex, convex hull, and extreme points as done (#7924)

YaelDillies committed 4 years ago

5f8cc8eb

feat(group_theory/order_of_element): Raising to a coprime power is a bijection (#7923)

tb65536 committed 4 years ago

e4ceee66

feat(measure_theory/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) (#7918)

RemyDegenne committed 4 years ago

f4991b97

chore(order/lattice): rename le_sup_left_of_le (#7856)

YaelDillies committed 4 years ago

b19c491a

feat(algebra/algebra/basic): define `restrict_scalars.linear_equiv` (#7807)

ocfnash committed 4 years ago

8e281044

feat(geometry/manifold/algebra/smooth_functions): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7749)

Nicknamen committed 4 years ago

a16650c4

Newer Older