leanprover-community/mathlib

Pull Requests Commits

playing with chilapla's examples

alexjbest committed 3 years ago

d0f90b61

feat(data/real/sqrt): add a few lemmas (#11003)

urkud committed 3 years ago

4ce0d047

chore(measure_theory): golf a proof (#11002)

urkud committed 3 years ago

694b3f85

refactor(analysis/seminorm): Weaken typeclasses (#10999)

YaelDillies committed 3 years ago

3362b1e2

feat(ring_theory/finiteness): prove that a surjective endomorphism of a finite module over a comm ring is injective (#10944)

alexjbest committed 3 years ago

cce09a6b

feat(field_theory/adjoin): `intermediate_field.to_subalgebra` distributes over supremum (#10937)

tb65536 committed 3 years ago

327bacc4

feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g (#10767)

ericrbg committed 3 years ago

e6f4852b

feat(combinatorics/simple_graph/basic): add lemmas about the neighbor set of a vertex in the complement graph (#7138)

agusakov committed 3 years ago

1107693b

ci(.github/workflows/*): cleanup after upload step (#11008)

bryangingechen committed 3 years ago

63a0936b

chore(tactic/norm_cast): minor cleanup (#10993)

digama0 committed 3 years ago

cf345987

feat(analysis/calculus): assorted simple lemmas (#10975)

urkud committed 3 years ago

1a57c79e

chore(algebra/algebra/*): add some `simp` lemmas (#10969)

ericrbg committed 3 years ago

35ede3d4

feat(field_theory/separable): add expand_eval and expand_monic (#10965)

riccardobrasca committed 3 years ago

7defe7df

feat(combinatorics/set_family/shadow): Upper shadow of a set family (#10956)

YaelDillies committed 3 years ago

2be37b00

feat(data/sigma/order): The lexicographical order has a bot/top (#10905)

YaelDillies committed 3 years ago

60c2b68c

feat(combinatorics/configuration): Define `line_count` and `point_count` (#10884)

tb65536 committed 3 years ago

87fa060c

feat(data/polynomial/ring_division): add `polynomial.card_le_degree_of_subset_roots` (#10824)

isadofschi committed 3 years ago

bd164c7f

feat(topology/algebra/group): definitionally better lattice (#10792)

eric-wieser committed 3 years ago

ec6d9a73

feat(linear_algebra/orientation): composing with linear equivs and determinant (#10737)

jsm28 committed 3 years ago

6e9b0112

chore(data/vector3): Make linter happy (#10998)

YaelDillies committed 3 years ago

34993236

feat(data/option): simple lemmas about orelse (#10972)

dwarn committed 3 years ago

72b4541a

feat(ring_theory/tensor_product): Supremum of finite dimensional subalgebras (#10922)

tb65536 committed 3 years ago

db1788c4

feat(algebraic_geometry): Prime spectrum is sober. (#10989)

erdOne committed 3 years ago

f3b380e4

chore(order/*): Change `order_hom` notation (#10988)

YaelDillies committed 3 years ago

086469f7

feat(ring_theory/integral_closure): The product of the leading coeff and the root is integral. (#10807)

erdOne committed 3 years ago

03062ea4

feat(data/list/count): countp of true and false (#10986)

b-mehta committed 3 years ago

2cfa052b

feat(field_theory/adjoin): add dim_bot, finrank_bot (#10964)

Sebastian-Monnet committed 3 years ago

08b13ec9

feat(data/list/count): count_le_length (#10982)

kmill committed 3 years ago

f4e46fd2

feat(order/complete_boolean_algebra): lemmas about binfi (#10852)

b-mehta committed 3 years ago

04779a32

feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820)

sgouezel committed 3 years ago

f00007dc

Older