two_smul'

Stream: mathlib4

[Michael Stoll]

What is the reason why docs#two_smul' is deprecated? I'm trying to generalize some things around quadratic maps (see this thread), and in this context, this is a very handy lemma (and is frequently suggested by exact?).

If there is a good reason to deprecate it, what would be a functional equivalent?

[Ruben Van de Velde]

Huh, no idea

[Ruben Van de Velde]

Apparently it used to be about bit0

[Eric Wieser]

It should be a special case of a lemma about ofNat_smul

[Michael Stoll]

@loogle "ofNat_smul"

[loogle]

:search: Matrix.conjTranspose_ofNat_smul, Matrix.conjTranspose_inv_ofNat_smul

[Michael Stoll]

These two do not look relevant...

[Michael Stoll]

@loogle ⊢ (?n : ?R) • ?x = (?n : ℕ) • ?x

[loogle]

Failure! Bot is unavailable

[Michael Stoll]

The web interface worked and gave 12 hits (docs#two_smul' among them), but nothing that would generalize two_smul' to arbitrary Nat literals.

[Edward van de Meent]

is natCast_zsmul relevant?

[Edward van de Meent]

maybe ofNat_zsmul ?

[Michael Stoll]

These are for conversion between scalar multiplication by naturals and integers; not between naturals and ring elements.

[Edward van de Meent]

ah right

[Edward van de Meent]

oops

[Yaël Dillies]

I'm adding the missing lemma in a pR

[Yaël Dillies]

Update: I can't find the PR but I do vividly remember writing the lemma. I will open a separate PR

[Eric Wieser]

I also remember writing the lemma

[Eric Wieser]

Maybe it's the nnrat floor PR?

[Yaël Dillies]

Pretty sure it was a PR of mine :thinking:

[Yury G. Kudryashov]

That's why I'm trying to cherry-pick small lemmas to separate PRs. Even if the main PR is stuck in review, the helper lemmas get merged (and it's easier to merge master later).

[Yaël Dillies]

#14997

[Eric Wieser]

That doesn't have the lemma we want about ofNat?

[Eric Wieser]

In fact, isn't that lemma just docs#nsmul_eq_smul_cast ?

[Yaël Dillies]

Damn, it's really hard to find lemmas when they are stated the wrong way :frown:

[Eric Wieser]

Loogle found it for me

[Michael Stoll]

I guess we also want an OfNat.ofNat version, if it is supposed to specialize to docs#two_smul' ?

[Ruben Van de Velde]

Yes

[Yaël Dillies]

I will update #14997

[Yaël Dillies]

Update: Updated