leanprover-community/mathlib

Pull Requests Commits

chore(algebra/group_power/lemmas): Lemmas about gsmul (#8618)

apurvnakade committed 4 years ago

7e8432d4

feat(linear_algebra/dimension): generalize inequalities and invariance of dimension to arbitrary rings (#8343)

kim-em committed 4 years ago

7265a4ee

feat(archive/imo): IMO 2006 Q3 (#8052)

peakpoint committed 4 years ago

15b14619

feat(linear_algebra/clifford_algebra/equivs): the equivalences preserve conjugation (#8739)

eric-wieser committed 4 years ago

5dc8bc16

fix(linear_algebra/basic): fix incorrect namespaces (#8757)

eric-wieser committed 4 years ago

dd5e779e

docs(overview): add weak-* topology (#8755)

PatrickMassot committed 4 years ago

d1720856

feat(measure_theory/strongly_measurable): define strongly measurable functions (#8623)

RemyDegenne committed 4 years ago

86fccaab

chore(algebra/big_operators): weaken assumption for multiset.exists_smul_of_dvd_count (#8758)

Ruben-VandeVelde committed 4 years ago

802859f2

feat(group_action/defs): add missing comp_hom smul instances (#8707)

eric-wieser committed 4 years ago

1efa3673

feat(ring_theory): the trace of an integral element is integral (#8702)

Vierkantor committed 4 years ago

4113db58

Revert "feat(field_theory/intermediate_field): generalize `algebra` instances"

Vierkantor committed 4 years ago

159e34ee

feat(field_theory/intermediate_field): generalize `algebra` instances

Vierkantor committed 4 years ago

4b525bf2

chore(tactic/rewrite_search): reuse rw_rules_p parser (#8752)

digama0 committed 4 years ago

902d3ac9

feat(analysis/calculus/deriv): prove `deriv_inv` at `x = 0` as well (#8748)

urkud committed 4 years ago

28a360a6

feat(topology/metric_space/basic): `emetric.ball x ∞ = univ` (#8745)

urkud committed 4 years ago

1c60e618

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

leanprover-community-bot committed 4 years ago

0e0a2404

chore(order/complete_lattice): golf some proofs (#8746)

urkud committed 4 years ago

ee3f8b8d

doc(tactic/simps): typo (#8751)

fpvandoorn committed 4 years ago

84554339

feat(algebra/algebra): `alg_{hom,equiv}.restrict_scalars` is injective (#8743)

Vierkantor committed 4 years ago

6fe5b552

doc({topology.algebra.weak_dual_topology, analysis.normed_space.weak_dual}): fix docstrings (#8710)

kkytola committed 4 years ago

e0bf9a16

feat(algebra/ordered_sub): define truncated subtraction in general (#8503)

fpvandoorn committed 4 years ago

23cf025c

feat(data/nat/pairing): add some `nat.pair` lemmas (#8740)

kex-y committed 4 years ago

0860c415

fix(transform_decl): fix namespace bug (#8733)

fpvandoorn committed 4 years ago

e6fda2ac

doc(tactic/simps): expand (#8729)

fpvandoorn committed 4 years ago

9a249eef

feat(topology/compact_open): the family of constant maps collectively form a continuous map (#8721)

ocfnash committed 4 years ago

6a83c7da

chore(topology/continuous_function/compact): relax typeclass assumptions for metric space structure on C(X, Y) (#8717)

ocfnash committed 4 years ago

3ac609b9

feat(topology/{continuous_function/bounded, metric_space/algebra}): new mixin classes (#8580)

hrmacbeth committed 4 years ago

0d59511a

feat(data/list/min_max): maximum is a fold, bounded prod (#8543)

pechersky committed 4 years ago

26590e97

feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536)

pechersky committed 4 years ago

4e7e7df8

feat(model_theory/basic): more substructure API, including subtype, map, and comap (#7937)

awainverse committed 4 years ago

15444e1f

Newer Older