dependent and

Stream: maths

[Ashvni Narayanan]

I want to define X to be Y ∧ Z, where Z is dependent on Y.

As an example, I want to define

import data.zmod.basic

def factors_through {n : ℕ} (χ : zmod n →* zmod R) (d : ℕ) : Prop :=
d ∣ n ∧ (d ∣ n → ∃ χ₀  : zmod d →* zmod R, χ = χ₀.comp (zmod.cast_hom hm (zmod n)))

Is there a way to do this? One way is to use Y ∧ (Y → Z). Is there anything simpler?

Thank you!

[Anne Baanen]

You could do it as a struct:

structure factors_through {n : ℕ} (χ : zmod n →* zmod R) (d : ℕ) : Prop :=
(dvd : d ∣ n)
(exists_coe : ∃ χ₀  : zmod d →* zmod R, χ = χ₀.comp (zmod.cast_hom dvd (zmod n)))

[Reid Barton]

You can also write \exists y : Y, Z y

[Reid Barton]

(or maybe h or hy would be a less confusing variable name)

[Ashvni Narayanan]

Ah, I see. I had completely forgotten about structures :relieved:
Both suggestions should work, thank you!