leanprover-community/mathlib3

Pull Requests Commits

Update src/linear_algebra/tensor_product.lean

antoinelab01 committed 3 years ago

Verified 9b5892e0

tensor_product.finite

antoinelab01 committed 3 years ago

afddfa75

feat(linear/algebra/tensor_product): the tensor product of finite modules is finite

antoinelab01 committed 3 years ago

d1fef947

feat(data/nat/totient): totient equals one iff (#13688)

ericrbg committed 3 years ago

8f604aa3

feat(category_theory/abelian): if D is abelian so is C ⥤ D (#13686)

kim-em committed 3 years ago

4e50b688

feat(data/fin/succ_pred): `fin` is an archimedean succ/pred order (#12792)

ericrbg committed 3 years ago

43e84cdd

feat(algebra/group_power/order): Add sq_zero_iff (#13670)

Smaug123 committed 3 years ago

4481a561

feat(analysis/normed_space/exponential): add `pi.exp_apply` (#13488)

eric-wieser committed 3 years ago

e2f56961

refactor(category_theory/monoidal): rearrange simp lemmas to work better with coherence (#13409)

kim-em committed 3 years ago

85075bcc

feat(analysis/convex/measure): a convex set is null-measurable (#13138)

urkud committed 3 years ago

9f75d75a

feat(data/nat/choose): add facts about the multiplicity of primes in the factorisation of central binomial coefficients (#9925)

Smaug123 committed 3 years ago

2c15ce14

feat(data/set/prod): add `set.eval_image_pi_subset` (#13613)

urkud committed 3 years ago

2825f353

chore(data/finsupp/fin): golf some proofs (#13607)

Ruben-VandeVelde committed 3 years ago

14b0e32b

feat(algebra/periodic): add lemmas `periodic.prod`, `periodic.smul`, `antiperiodic.smul` (#13496)

ocfnash committed 3 years ago

b7538a30

feat(set_theory/game/pgame): remove nolint (#13680)

vihdzp committed 3 years ago

4bfae3d8

feat(dynamics/periodic_pts): `pow_smul_eq_iff_minimal_period_dvd` (#13676)

tb65536 committed 3 years ago

9e8d1075

feat(topology/algebra): actions on the opposite type are continuous (#13671)

eric-wieser committed 3 years ago

7231172e

feat(ring_theory/witt_vector/frobenius): add `witt_vector.frobenius_equiv` (#13666)

eric-wieser committed 3 years ago

ed10ba23

feat(data/zmod/basic): `-1 : zmod n` lifts to `n - 1` (#13665)

tb65536 committed 3 years ago

6d3ca07a

feat(dynamics/periodic_pts): Iteration is injective below the period (#13660)

tb65536 committed 3 years ago

ad0a3e66

feat(analysis/complex/roots_of_unity): arg of a primitive root (#13583)

ericrbg committed 3 years ago

6710d655

feat(algebra/order/hom/ring): There's at most one hom between linear ordered fields (#13601)

YaelDillies committed 3 years ago

b35ed400

feat(number_theory/legendre_symbol/quadratic_reciprocity): Alternate forms of `exists_sq_eq_neg_one` (#13594)

vihdzp committed 3 years ago

d795ea4b

feat(logic/basic): `congr_fun` for heterogeneous equality (#13591)

vihdzp committed 3 years ago

e251ef77

feat(algebra/big_operators/basic): mk0_prod (#13582)

ericrbg committed 3 years ago

e059fdf9

feat(special_functions/gamma): recurrence relation for Gamma function (#13156)

loefflerd committed 3 years ago

f02c7844

feat(group_theory/subgroup/basic): Cyclic subgroups are commutative (#13663)

tb65536 committed 3 years ago

ef3769db

feat(order/filter): add `filter.coprod_bot` etc (#13662)

urkud committed 3 years ago

b0fe3cd2

feat(group_theory/group_action/basic): More API for `quotient_action` (#13661)

tb65536 committed 3 years ago

feb9aed4

refactor(analysis/convex/basic): rewrite a few proofs (#13658)

urkud committed 3 years ago

46563c5c

Older