leanprover-community/mathlib3

Pull Requests Commits

Many homeless lemmas

TwoFX committed 4 years ago

2f676b25

feat(category_theory/subobject): proof golf and some API

TwoFX committed 4 years ago

88e27fac

chore(category_theory/subobject): split off specific subobjects

TwoFX committed 4 years ago

90f75e57

feat(algebra/algebra/basic algebra/module/basic): add 3 lemmas m • (1 : R) = ↑m (#7094)

adomani committed 4 years ago

5694309f

feat(analysis/special_functions/exp_log): add `continuity` attribute to `continuous_exp` (#7157)

benjamindavidson committed 4 years ago

fbf62199

feat(measure_theory/interval_integral): variants of integral_comp lemmas (#7103)

benjamindavidson committed 4 years ago

1442f70a

feat(topology/continuous_function): comp_right_* (#7145)

kim-em committed 4 years ago

fc8e18c1

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

leanprover-community-bot committed 4 years ago

383f591e

feat(analysis/normed_space/finite_dimension): set of `f : E →L[𝕜] F` of rank `≥n` is open (#7022)

urkud committed 4 years ago

c6e62cfe

feat(linear_algebra/eigenspace): define the maximal generalized eigenspace (#7125)

ocfnash committed 4 years ago

a83230e0

feat(geometry/manifold): a manifold with σ-countable topology has second countable topology (#6948)

urkud committed 4 years ago

026150f3

chore(analysis/normed_space/inner_product): simplify two proofs (#7149)

bentoner committed 4 years ago

6b3803d6

chore(*): speedup slow proofs (#7148)

sgouezel committed 4 years ago

363a286b

feat(analysis/normed_space/banach): a range with closed complement is itself closed (#6972)

sgouezel committed 4 years ago

7e933678

feat(data/zsqrtd/basic): add some lemmas about norm (#7114)

Ruben-VandeVelde committed 4 years ago

d39c3a26

feat(group_theory/is_free_group): promote `is_free_group.lift'` to an equiv (#7110)

eric-wieser committed 4 years ago

7ae2af63

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

leanprover-community-bot committed 4 years ago

575b791e

feat(category_theory/action): currying (#7085)

dwarn committed 4 years ago

7138d354

feat(tactic/itauto): Complete intuitionistic prover (#7057)

digama0 committed 4 years ago

e269dbc1

feat(combinatorics/simple_graph/strongly_regular): add definition of strongly regular graph and proof that complete graph is SRG (#7044)

agusakov committed 4 years ago

8efb93b1

feat(category_theory/subobjects): improvements to API (#6932)

kim-em committed 4 years ago

309e3b08

chore(data/list/basic): avoid the axiom of choice (#7135)

eric-wieser committed 4 years ago

763c5c3a

feat(algebra/category/Module): arbitrary colimits (#7099)

kim-em committed 4 years ago

fe5d6604

chore(data/fin): add simp lemmas about 1 and cast_{pred, succ} (#7067)

eric-wieser committed 4 years ago

0ec9cd8d

chore(data/set_like): Add coe_strict_mono and coe_mono (#7004)

eric-wieser committed 4 years ago

dd2466ce

feat(category_theory/preadditive): a category induced from a preadditive category is preadditive (#6883)

kim-em committed 4 years ago

362844dc

feat(data/option/basic): option valued choice operator (#7101)

kim-em committed 4 years ago

aa1fa0b2

feat(data/fintype): golf, move and dualise proof (#7126)

b-mehta committed 4 years ago

6610e8f5

chore(linear_algebra/multilinear): relax requirements on `multilinear_map.pi_ring_equiv` (#7117)

eric-wieser committed 4 years ago

991dc260

feat(test/integration): update with new examples (#7105)

benjamindavidson committed 4 years ago

0b52522e

Older