leanprover-community/mathlib

Pull Requests Commits

Remove import tactic

prakol16 committed 3 years ago

18851eac

Update pairing.lean

prakol16 committed 3 years ago

Verified 95441a7f

Update pairing.lean

prakol16 committed 3 years ago

Verified 2f71e73e

Update pairing.lean

prakol16 committed 3 years ago

Verified 8d6ff383

Update pairing.lean

prakol16 committed 3 years ago

Verified 141a8c7e

Merge branch 'master' of https://github.com/leanprover-community/mathlib into efficient_mkpair

prakol16 committed 3 years ago

5357c441

Merge branch 'encode_binary_lemmas' of https://github.com/leanprover-community/mathlib into efficient_mkpair

prakol16 committed 3 years ago

54b7f356

feat(model_theory/syntax, semantics): Substitution of variables in terms and formulas (#13632)

awainverse committed 3 years ago

bb45687b

chore(set_theory/game/basic): golf proof (#13810)

vihdzp committed 3 years ago

a34ee7b7

feat(set_theory/surreal/basic): add `pgame.numeric.left_lt_right` (#13809)

vihdzp committed 3 years ago

24bc2e1c

feat(ring_theory): factorize a non-unit into irreducible factors without multiplying a unit (#13682)

alreadydone committed 3 years ago

a70166a3

chore(set_theory/game/basic): fix a single space (#13806)

vihdzp committed 3 years ago

059c8eb7

chore(data/polynomial): use dot notation for sub lemmas (#13799)

alexjbest committed 3 years ago

89102286

feat(model_theory/graph): First-order language and theory of graphs (#13720)

awainverse committed 3 years ago

e56b8fea

chore(topology/algebra/valuation): use forgetful inheritance pattern for valued fields (#13691)

ocfnash committed 3 years ago

1d4ed4a5

feat(model_theory/encoding): A bound on the number of bounded formulas (#13616)

awainverse committed 3 years ago

90bd6f54

feat(model_theory/syntax, semantics): A theory of infinite structures (#13580)

awainverse committed 3 years ago

9ce5e95a

feat(model_theory/semantics, satisfiability): Complete Theories (#13558)

awainverse committed 3 years ago

812518d9

feat(analysis/normed_space/pointwise): Addition of balls (#13381)

YaelDillies committed 3 years ago

812e17f8

feat(data/finset/basic): A finset that's a subset of a `directed` union is contained in one element (#13727)

awainverse committed 3 years ago

a54db9a4

chore(analysis/normed/group/basic): add `nnnorm_sum_le_of_le` (#13795)

eric-wieser committed 3 years ago

8624f6db

feat(model_theory/language_map, bundled): Reducts of structures (#13745)

awainverse committed 3 years ago

8360f2c8

chore(analysis/normed_space/operator_norm): move `continuous_linear_map.op_norm_lsmul` into the correct section (#13790)

eric-wieser committed 3 years ago

50c30283

feat(ring_theory/valuation/extend_to_localization): Extending valuations to localizations. (#13610)

adamtopaz committed 3 years ago

64b3576f

feat(number_theory/primes_congruent_one): attempt to golf (#13787)

alexjbest committed 3 years ago

fe2917a4

feat(analysis/*): a sample of easy useful lemmas (#13697)

sgouezel committed 3 years ago

a3beb628

chore(analysis/convex): move `convex_on_norm`, change API (#13631)

urkud committed 3 years ago

7373832e

feat(analysis/normed_space/pi_Lp): add lemmas about `pi_Lp.equiv` (#13569)

eric-wieser committed 3 years ago

ce79a27b

feat(algebra/order/monoid_lemmas_zero_lt): add instances (#13376)

astrainfinita committed 3 years ago

e5612640

feat(set_theory/cardinal/basic): cardinality of a powerset (#13786)

eric-wieser committed 3 years ago

58552fe0

Older