leanprover-community/mathlib3

Pull Requests Commits

back to star_ring_equiv

dupuisf committed 3 years ago

5fe3c442

some more progress

dupuisf committed 3 years ago

47303729

alg hom and alg equiv

dupuisf committed 3 years ago

f4581b1b

star_ring_hom and star_ring_equiv

dupuisf committed 3 years ago

f11702c1

feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626)

eric-wieser committed 3 years ago

ae10dced

feat(analysis/inner_product_space): Gram-Schmidt Basis (#14514)

abentkamp committed 3 years ago

67da2721

fix(data/rat/basic): Remove incorrect simp attribute (#14765)

Jon Eugster committed 3 years ago

988f160d

feat(linear_algebra/clifford_algebra/fold): Add recursors for folding along generators (#14619)

eric-wieser committed 3 years ago

6c46641d

feat(set_theory/game/ordinal): addition of ordinals on games matches natural addition (#14298)

vihdzp committed 3 years ago

7584a104

feat(data/nat/basic): add a few lemmas (#14718)

user7230724 committed 3 years ago

b05d8459

feat(algebra/homology,category_theory/abelian): exact_comp_mono_iff (#14410)

TwoFX committed 3 years ago

3feb151c

feat(analysis/asymptotics): define `is_Theta` (#14567)

urkud committed 3 years ago

6834a24e

feat(analysis/special_functions/arsinh): add lemmas, review API (#14668)

urkud committed 3 years ago

0053e3c5

refactor(set_theory/game/*): Delete `winner.lean` (#14271)

vihdzp committed 3 years ago

22f32559

chore(*): Bump to Lean 3.43.0 (#14684)

urkud committed 3 years ago

f991b4d4

feat(data/polynomial/erase_lead): `lt_nat_degree_of_mem_erase_lead_support` (#14745)

tb65536 committed 3 years ago

c81c6c91

feat(analysis/special_functions/integrals): Add integral_cpow (#14491)

khwilson committed 3 years ago

ea2dbcbb

feat(algebra/group/pi): Technical casework lemma for when two binomials are equal to each other (#14400)

tb65536 committed 3 years ago

71450437

chore(data/nat/factorization/basic): delete two duplicate lemmas (#14754)

stuart-presnell committed 3 years ago

665cec25

feat(representation_theory/Action): a few lemmas about the rigid structure of Action (#14620)

antoinelab01 committed 3 years ago

a5832444

feat(order/rel_classes): an irreflexive order on a subsingleton type is a well order (#14601)

vihdzp committed 3 years ago

c4ef20e9

fix(tactic/congrm): support multiple binders (#14753)

gebner committed 3 years ago

94fa33b4

chore(analysis/normed): move `normed.normed_field` to `normed.field.basic` (#14747)

urkud committed 3 years ago

430da94f

feat(data/finite/set): `finite` instances for set constructions (#14673)

kmill committed 3 years ago

6a0f9674

chore(a few random files): golfing using the new tactic `congrm` (#14593)

adomani committed 3 years ago

8eaeec26

refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213)

YaelDillies committed 3 years ago

34ce7847

feat(dynamics/periodic_pts): `chain.pairwise` on orbit (#12991)

vihdzp committed 3 years ago

bbca2890

chore(analysis/normed/normed_field): golf 2 proofs (#14746)

urkud committed 3 years ago

46614736

chore(set_theory/ordinal/basic): golf ordinal addition definition (#14744)

vihdzp committed 3 years ago

dccdef6b

feat(analysis/normed_space): range of `norm` (#14740)

urkud committed 3 years ago

d2bfb32b

Older